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

$ ./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

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;
}