CryptoMiniSat 5

Newest version HERE.

Build instructions HERE.

Source is available here. File a bug report or create pull requests.

Referencing in Pulibcations

Always reference our SAT 2009 conference paper.
BibTex record HERE.

Features

CryptoMiniSat is a modern, multi-threaded, feature-rich, simplifying SAT solver. Highlights:

  • Instance simplification at every point of the search (inprocessing)
  • Many configurable parameters to tune to specific need
  • Collection of statistical data to sqlite database
  • Clean C++ and python interfaces

Techniques Used

Here is a non-exhaustive list of techniques used in CryptoMiniSat 4:

  • Variable elimination and replacement, strengthening, subsumption, vivification
  • On-the-fly stamping, literal caching, hyper-binary resolution and transitive reduction during failed literal probing
  • Bounded variable addition with hack to allow 2-literal diff
  • DRAT-based unsatisfiable proof logging
  • XOR recovery and manipulation (NOTE: uses the M4RI library that is GPL, if you want LGPL, compile without it)
  • Precise time- and memory tracking. No time or memory-outs on weird CNFs
  • Precise usefulness tracking of all clauses
  • Clause usefulness-based redundant clause removal. Glues are not used by default, but glues are tracked and can be used (command line option)
  • Variable renumbering and variable number hiding. Thanks to this, XOR clauses are cut and the added variables are always consistently displayed to the user.
  • SQL-based data logging and AJAX-based powerful data display
  • And of course many-many more

Use

Command-line use

which means that the problem has 3 variables and 2 clauses. The problem is satisfiable and a solution is v1 = True, v2 = True, v3 = False. There are 3 solutions:

This lists all the solutions and then finishes with “UNSATISFIABLE” meaning there are certainly no more solutions than those listed.

Python interface

It’s intuitive and fun to use:

C++ interface

Usage is pretty simple, and the header files have been significantly cleaned up: