Need help with cryptominisat?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

575 Stars 142 Forks Other 15.0K Commits 9 Opened issues


An advanced SAT solver

Services available


Need anything else?

Contributors list

License: MIT Liunux&Mac build Windows build build Coverity Codacy Badge Docker Hub

CryptoMiniSat SAT solver

This system provides CryptoMiniSat, an advanced incremental SAT solver. The system has 3 interfaces: command-line, C++ library and python. The command-line interface takes a cnf as an input in the DIMACS format with the extension of XOR clauses. The C++ and python interface mimics this and also allows for incremental use: assumptions and multiple

calls. A C compatible wrapper is also provided.

When citing, always reference our SAT 2009 conference paper, bibtex record is here.


Please read LICENSE.txt for a discussion. Everything that is needed to build is MIT licensed. The M4RI library (not included) is GPL, so in case you have M4RI installed, you must build with

in case you need a pure MIT build.

Docker usage

To run on file

cat myfile.cnf | docker run --rm -i msoos/cryptominisat

To run on the file

by mounting it (may be faster):
docker run --rm -v /home/myfolder/myfile.cnf.gz:/f msoos/cryptominisat f

Compiling in Linux

To build and install, issue:

sudo apt-get install build-essential cmake
# not required but very useful
sudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev libsqlite3-dev help2man
tar xzvf cryptominisat-version.tar.gz
cd cryptominisat-version
mkdir build && cd build
cmake ..
sudo make install
sudo ldconfig

Compiling in Mac OSX

First, you must get Homebrew from then:

brew install cmake boost zlib
tar xzvf cryptominisat-version.tar.gz
cd cryptominisat-version
mkdir build && cd build
cmake ..
sudo make install

Compiling in Windows

You will need python installed, then for Visual Studio 2015:

C:\> [ download ]
C:\> unzip
C:\> rename cryptominisat-version cms
C:\> cd cms
C:\cms> mkdir build
C:\cms> cd build

C:\cms\build> [ download ] C:\cms\build> unzip C:\cms\build> mkdir boost_1_59_0_install C:\cms\build> cd boost_1_59_0 C:\cms\build\boost_1_59_0> bootstrap.bat --with-libraries=program_options C:\cms\build\boost_1_59_0> b2 --with-program_options address-model=64 toolset=msvc-14.0 variant=release link=static threading=multi runtime-link=static install --prefix="C:\cms\build\boost_1_59_0_install" > boost_install.out C:\cms\build\boost_1_59_0> cd ..

C:\cms\build> git clone C:\cms\build> cd zlib C:\cms\build\zlib> git checkout v1.2.8 C:\cms\build\zlib> mkdir build C:\cms\build\zlib> mkdir myinstall C:\cms\build\zlib> cd build C:\cms\build\zlib\build> cmake -G "Visual Studio 14 2015 Win64" -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=C:\cms\build\zlib\myinstall .. C:\cms\build\zlib\build> msbuild /t:Build /p:Configuration=Release /p:Platform="x64" zlib.sln C:\cms\build\zlib\build> msbuild INSTALL.vcxproj C:\cms\build> cd ....

C:\cms\build> cmake -G "Visual Studio 14 2015 Win64" -DCMAKE_BUILD_TYPE=Release -DSTATICCOMPILE=ON -DZLIB_ROOT=C:\cms\build\zlib\myinstall -DBOOST_ROOT=C:\cms\build\boost_1_59_0_install .. C:\cms\build> cmake --build --config Release .

You now have the static binary under


Command-line usage

Let's take the file:

p cnf 3 3
1 0
-2 0
-1 2 3 0

The file has 3 variables and 3 clauses, this is reflected in the header

p cnf 3 3
which gives the number of variables as the first number and the number of clauses as the second. Every clause is ended by '0'. The clauses say: 1 must be True, 2 must be False, and either 1 has to be False, 2 has to be True or 3 has to be True. The only solution to this problem is:
cryptominisat5 --verb 0 file.cnf
v 1 -2 3 0

Which means, that setting variable 1 True, variable 2 False and variable 3 True satisfies the set of constraints (clauses) in the CNF. If the file had contained:

p cnf 3 4
1 0
-2 0
-3 0
-1 2 3 0

Then there is no solution and the solver returns


Incremental Python Usage

The python module works with both Python 2 and Python 3. It must be compiled as per (notice "python-dev"):

sudo apt-get install build-essential cmake
sudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev libsqlite3-dev help2man
sudo apt-get install python3-setuptools python3-dev
tar xzvf cryptominisat-version.tar.gz
cd cryptominisat-version
mkdir build && cd build
cmake ..
sudo make install
sudo ldconfig

You can then use it in incremental mode as:

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

We can also try to assume any variable values for a single solver run: ```

sat, solution = s.solve([-3]) print sat False print solution None sat, solution = s.solve() print sat True print solution (None, True, False, True) ```

For more detailed usage instructions, please see the README.rst under the


Incremental Library Usage

The library uses a variable numbering scheme that starts from 0. Since 0 cannot be negated, the class

is used as:
Lit(variable_number, is_negated)
. As such, the 1st CNF above would become:
using std::vector;
using namespace CMSat;

int main() { SATSolver solver; vector clause;

//Let's use 4 threads

//We need 3 variables. They will be: 0,1,2
//Variable numbers are always trivially increasing

//add "1 0"
clause.push_back(Lit(0, false));

//add "-2 0"
clause.push_back(Lit(1, true));

//add "-1 2 3 0"
clause.push_back(Lit(0, true));
clause.push_back(Lit(1, false));
clause.push_back(Lit(2, false));

lbool ret = solver.solve();
assert(ret == l_True);
<< "Solution is: "
<< solver.get_model()[0]
<< ", " << solver.get_model()[1]
<< ", " << solver.get_model()[2]
<< std::endl;

//assumes 3 = FALSE, no solutions left
vector<lit> assumptions;
assumptions.push_back(Lit(2, true));
ret = solver.solve(&amp;assumptions);
assert(ret == l_False);

//without assumptions we still have a solution
ret = solver.solve();
assert(ret == l_True);

//add "-3 0"
//No solutions left, UNSATISFIABLE returned
clause.push_back(Lit(2, true));
ret = solver.solve();
assert(ret == l_False);

return 0;

} </assert.h>

The library usage also allows for assumptions. We can add these lines just before the

return 0;
above: ``` vector assumptions; assumptions.pushback(Lit(2, true)); lbool ret = solver.solve(&assumptions); assert(ret == lFalse);

lbool ret = solver.solve(); assert(ret == l_True); ```

Since we assume that variable 2 must be false, there is no solution. However, if we solve again, without the assumption, we get back the original solution. Assumptions allow us to assume certain literal values for a specific run but not all runs -- for all runs, we can simply add these assumptions as 1-long clauses.

Multiple solutions

To find multiple solutions to your problem, just run the solver in a loop and ban the previous solution found:

while(true) {
    lbool ret = solver->solve();
    if (ret != l_True) {
        assert(ret == l_False);
        //All solutions found.

//Use solution here. print it, for example.

//Banning found solution
vector<lit> ban_solution;
for (uint32_t var = 0; var &lt; solver-&gt;nVars(); var++) {
    if (solver-&gt;get_model()[var] != l_Undef) {
            Lit(var, (solver-&gt;get_model()[var] == l_True)? true : false));


The above loop will run as long as there are solutions. It is highly suggested to only add into the new clause(

above) the variables that are "important" or "main" to your problem. Variables that were only used to translate the original problem into CNF should not be added. This way, you will not get spurious solutions that don't differ in the main, important variables.

Rust bindings

To build the Rust bindings:

git clone
cd cryptominisat-rs
cargo build --release
cargo test

You can use it as per the README in that repository. To include CryptoMiniSat in your Rust project, add the dependency to your

cryptominisat = { git = "", branch= "master" }

You can see an example project using CryptoMiniSat in Rust here.

Preprocessor usage

Run cryptominisat5 as:

./cryptominisat5 -p1 input.cnf simplified.cnf
some_sat_solver simplified.cnf > output
./cryptominisat5 -p2 output


is a SAT solver of your choice that outputs a solution in the format of:
v [solution] 0



You can tune the schedule of simplifications by issuing

--sched "X,Y,Z..."
. The default schedule for preprocessing is:
handle-comps,scc-vrepl, cache-clean, cache-tryboth,sub-impl, intree-probe, probe,
sub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl,occ-backw-sub-str,
occ-xor, occ-clean-implicit, occ-bve, occ-bva, occ-gates,str-impl, cache-clean,
sub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl,str-impl, sub-impl,
sub-str-cls-with-bin, occ-backw-sub-str, occ-bve,check-cache-size, renumber

It is a good idea to put

as late as possible, as it renumbers the variables for memory usage reduction.

Gauss-Jordan elimination

Since CryptoMiniSat 5.8, Gauss-Jordan elimination is compiled into the solver by default. However, it will turn off automatically in case the solver observes GJ not to perform too well. To use Gaussian elimination, provide a CNF with xors in it (either in CNF or XOR+CNF form) and either run with default setup, or, tune it to your heart's desire:

Gauss options:
  --iterreduce arg (=1)       Reduce iteratively the matrix that is updated.We
                              effectively are moving the start to the last
                              column updated
  --maxmatrixrows arg (=3000) Set maximum no. of rows for gaussian matrix. Too
                              large matrixes should be discarded for reasons of
  --autodisablegauss arg (=1) Automatically disable gauss when performing badly
  --minmatrixrows arg (=5)    Set minimum no. of rows for gaussian matrix.
                              Normally, too small matrixes are discarded for
                              reasons of efficiency
  --savematrix arg (=2)       Save matrix every Nth decision level
  --maxnummatrixes arg (=3)   Maximum number of matrixes to treat.

In particular, you may want to set

--autodisablegauss 0
in case you are sure it'll help.


For testing you will need the GIT checkout and build as per:

sudo apt-get install build-essential cmake git
sudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev libsqlite3-dev help2man
sudo apt-get install git python3-pip python3-setuptools python3-dev
sudo pip3 install --upgrade pip
sudo pip3 install lit
git clone
cd cryptominisat
git submodule update --init
mkdir build && cd build
make -j4
make test
sudo make install
sudo ldconfig


Build for test as per above, then:

cd ../cryptominisat/scripts/fuzz/


Build and use instructions below. Please see the associated blog post for more information.

# prerequisites on a modern Debian/Ubuntu installation
sudo apt-get install build-essential cmake git
sudo apt-get install zlib1g-dev libsqlite3-dev
sudo apt-get install libboost-program-options-dev
sudo apt-get install python3-pip
sudo pip3 install sklearn pandas numpy lit matplotlib

getting the code

git clone cd cryptominisat git checkout crystalball git submodule update --init mkdir build && cd build ln -s ../scripts/crystal/* . ln -s ../scripts/build_scripts/* .

Let's get an unsatisfiable CNF

wget gunzip goldb-heqc-i10mul.cnf.gz

Gather the data, denormalize, label, output CSV,

create the classifier, generate C++,

and build the final SAT solver

./ --csv goldb-heqc-i10mul.cnf [...compilations and the full data pipeline...]

let's use our newly built tool

we are using configuration number short:3 long:3

./cryptominisat5 --predshort 3 --predlong 3 goldb-heqc-i10mul.cnf [ ... ] s UNSATISFIABLE

Let's look at the data

cd goldb-heqc-i10mul.cnf-dir sqlite3 mydata.db sqlite> select count() from sum_cl_use; 94507

The CNFs go through the following set of transformations to become the generated code:

  1. ./cryptominisat
    dumps the data. Options:
    --cldatadumpratio 0.08
    --gluecut0 100
  2. ./drat-trim
  3. ./
  4. ./
  5. ./
    , etc.
  6. ./
    . Options:
  7. ./
  8. ./
  9. ./

Configuring a build for a minimal binary&library

The following configures the system to build a bare minimal binary&library. It needs a compiler, but nothing much else:


CMake Arguments

The following arguments to cmake configure the generated build artifacts. To use, specify options prior to running make in a clean subdirectory:

cmake  ..
    -- statically linked library and binary. You must build&link
    with the same
    setting as well. You can get the BreakID library from our GitHub repository
    -- Gauss-Jordan Elimination support. On by default.
  • -DSTATS=
    -- advanced statistics (slower)
    -- test suite support
  • -DMIT=
    -- MIT licensed components only
  • -DNOM4RI=
    -- without toplevel Gauss-Jordan Elimination support
    -- abort if M4RI is not present
    -- no gzip DIMACS input support
    -- only the simple binary is built
    -- no extended valgrind memory checking support
    -- more memory available for clauses (but slower on most problems)

Getting learnt clauses

As an experimental feature, you can get the learnt clauses from the system with the following code, where

is filled with learnt clauses every time
is called. The example below will eventually return all clauses of size 4 or less. You can call
at any time.
SATSolver s;
//fill the solver, run solve, etc.

//Get all clauses of size 4 or less


vector lits; bool ret = true; while (ret) { bool ret = s->get_next_small_clause(lits); if (ret) { //deal with clause in "lits" add_to_my_db(lits); } } s->end_getting_small_clauses();

C usage

See src/ for details. This is an experimental feature.

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.