CryptoMiniSat 4

Download and build

Newest version is 4.5.3
Source tarball as well as precompiled Linux binary is here.

For building you will need cmake. It’s also best to have zlib and the program options Boost library installed:

Features

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

  • Instance simplification at every point of the search (inprocessing)
  • Over 100 configurable parameters to tune to specific need
  • Collection of statistical data to MySQL database + javascript-based visualization of it
  • Clean C++ and python interfaces

Source code

The source is available here.You can file bug reports and create pull requests there.

Improvements and techniques

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
  • DRUP-based unsatisfiable proof logging
  • Gate-based clause shortening and removal
  • 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: