CryptoMiniSat 5 | Wonderings of a SAT geek

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

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

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

>>> 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 <cryptominisat4/cryptominisat.h>
#include <assert.h>
#include <vector>
using std::vector;
using namespace CMSat;

int main()
{
    Solver solver;
    solver.set_num_threads(4);
    vector<Lit> 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;
}

#include <cryptominisat4/cryptominisat.h>

#include <assert.h>

#include <vector>

using std::vector;

using namespace CMSat;

int main()

{

Solver solver;

solver.set_num_threads(4);

vector<Lit> 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;

}