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 solve calls. A C and a Rust compatible wrapper is also provided.

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

Compiling

Use of the release binaries is strongly encouraged. The second best thing to use is Nix. Simply install nix and then:

nix shell github:msoos/cryptominisat

Then you will have the cryptominisat5 binary available and ready to use.

Building from source

The build uses CMake and downloads and compiles its cadical and cadiback dependencies from GitHub, so it needs network access (or see -Dcadical_DIR below). GMP and pkg-config are required, zlib is optional (for reading gzipped CNFs). Install system packages:

# Debian/Ubuntu
sudo apt-get install build-essential cmake ninja-build git pkg-config \
          libgmp-dev zlib1g-dev

# macOS (brew)
brew install cmake ninja pkgconf gmp

# Windows: install MSYS2 (https://www.msys2.org/), then from the MINGW64 shell:
pacman -S mingw-w64-x86_64-gcc mingw-w64-x86_64-cmake mingw-w64-x86_64-ninja \
          mingw-w64-x86_64-pkgconf mingw-w64-x86_64-gmp mingw-w64-x86_64-zlib git

Then build (same commands on Linux, macOS, and Windows/MSYS2):

git clone https://github.com/msoos/cryptominisat
cd cryptominisat
mkdir build && cd build
cmake -G Ninja -DCMAKE_BUILD_TYPE=Release ..
cmake --build .

For a fully static binary (no shared-library or DLL dependencies at runtime), add -DBUILD_SHARED_LIBS=OFF:

cmake -G Ninja -DCMAKE_BUILD_TYPE=Release -DBUILD_SHARED_LIBS=OFF ..
cmake --build .

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
s SATISFIABLE
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 s UNSATISFIABLE.

Incremental Python Usage

The python module works with Python 3. Just execute:

pip3 install pycryptosat

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)
True
>>> print(solution)
(None, True, False, True)
>>> sat, solution = s.solve([-3])  # assume var 3 = False → UNSAT
>>> print(sat)
False
>>> sat, solution = s.solve()      # without assumption → still SAT
>>> print(sat)
True
>>> s.add_clause([-3])             # permanently add -3
>>> sat, solution = s.solve()
>>> print(sat)
False

Solver options such as Solver(options={"maxmatrixrows": "5000"}) are listed in python/README.md.

To build the Python package from source, install the system packages listed under Building from source, then:

git clone https://github.com/msoos/cryptominisat
cd cryptominisat
pip install .

Incremental Library Usage

The library uses a variable numbering scheme that starts from 0. Since 0 cannot be negated, the class Lit is used as: Lit(variable_number, is_negated). As such, the 1st CNF above would become:

#include <cryptominisat5/cryptominisat.h>
#include <assert.h>
#include <iostream>
#include <vector>
using std::vector;
using namespace CMSat;

int main()
{
    SATSolver solver;
    vector<Lit> clause;

    //Let's use 4 threads
    solver.set_num_threads(4);

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

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

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

    //add "-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);
    std::cout
    << "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(&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.clear();
    clause.push_back(Lit(2, true));
    solver.add_clause(clause);
    ret = solver.solve();
    assert(ret == l_False);

    return 0;
}

In the example above, when we assume that variable 3 (index 2) is 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, as done with "-3 0" at the end.

Command-line options can also be set from the library with set_option(name, value), where the name is the option without the leading --. It must be called before any variable or clause is added, e.g. right after set_num_threads(4) above:

solver.set_option("maxmatrixrows", "5000");
solver.set_option("polar", "rnd");

It throws std::invalid_argument on an unknown option or bad value, and std::runtime_error if called too late. The options available are listed in python/README.md, and returned by SATSolver::get_option_names().

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.
        exit(0);
    }

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

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

The above loop will run as long as there are solutions. It is highly suggested to only add into the new clause (ban_solution 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 https://github.com/msoos/cryptominisat-rs/
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 Cargo.toml file:

cryptominisat = { git = "https://github.com/msoos/cryptominisat-rs", branch= "master" }

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

Preprocessing

If you wish to use CryptoMiniSat as a preprocessor, we encourage you to try out our model counting preprocessor, Arjun.

Proof Verification

CryptoMiniSat emits XLRUP proofs that can be checked directly by the formally verified checker cake_xlrup from meelgroup/frat-xor:

./cryptominisat5 input.cnf proof.xlrup
./cake_xlrup --no-binary input.cnf proof.xlrup

cake_xlrup prints s VERIFIED on success. With --xlrup 2 the proof is written in the smaller, faster binary XLRUP encoding, which cake_xlrup reads by default:

./cryptominisat5 --xlrup 2 input.cnf proof.xlrupb
./cake_xlrup input.cnf proof.xlrupb

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 <options> ..

• -Dcadical_DIR=<path> -- a pre-built CaDiCaL: its CMake build directory or install prefix. Fetched from GitHub and built if not set.
• -Dcadiback_DIR=<path> -- same, for CaDiBack.
• -DBUILD_SHARED_LIBS=<ON/OFF> -- build shared (ON, default) or static (OFF) library and binary.
• -DLARGEMEM=<ON/OFF> -- more memory available for clauses (but slower on most problems)
• -DIPASIR=<ON/OFF> -- Build libipasircryptominisat5.so for IPASIR interface support
• -DNOZLIB=<ON/OFF> -- build without zlib, i.e. without gzipped CNF support
• -DENABLE_TESTING=<ON/OFF> -- test suite support
• -DNOCADICAL=ON -- build without CaDiCaL and CaDiBack. Backbone simplification becomes a no-op.

C usage

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

License

CryptoMiniSat is MIT licensed.