Newest version HERE. Python package HERE.

Build instructions HERE.

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

Referencing in Publications

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

$ ./cryptominisat --verb 0 problem.cnf
s SATISFIABLE
v 1 2 -3 0
$ cat problem.cnf
p cnf 3 2
1 2 3 0
-3 0

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:

$ ./cryptominisat --verb 0 --maxsol 10 problem.cnf
s SATISFIABLE
v 1 2 -3 0
s SATISFIABLE
v 1 -2 -3 0
s SATISFIABLE
v -1 2 -3 0
s UNSATISFIABLE

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

Python interface

IPython package HERE. It’s intuitive and fun to use:

>>> from pycryptosat import Solver
>>> s = Solver()
>>> s.add_clause([-1])
>>> s.add_clause([1, 2])
>>> sat, solution = s.solve()
>>> print sat
True
>>> print solution[1]
False
>>> print solution[2]
True

C++ interface

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

#include 
#include 
#include 
using std::vector;
using namespace CMSat;

int main()
{
    Solver solver;
    solver.set_num_threads(4);
    vector clause;

    //adds "1 0"
    clause.push_back(Lit(0, false));
    solver.add_clause(clause);

    //adds "-2 0"
    clause.clear();
    clause.push_back(Lit(1, true));
    solver.add_clause(clause);

    //adds "-1 2 3 0"
    clause.clear();
    clause.push_back(Lit(0, true));
    clause.push_back(Lit(1, false));
    clause.push_back(Lit(2, false));
    solver.add_clause(clause);

    lbool ret = solver.solve();
    assert(ret == l_True);
    assert(solver.get_model()[0] == l_True);
    assert(solver.get_model()[1] == l_False);
    assert(solver.get_model()[2] == l_True);

    return 0;
}