CryptoMiniSat 5.0.0, after winning the incremental track at SAT Competition 2016 and getting 3rd place at the parallel track, has been released. The new solver contains a number of important additions. The most important are that the solver can now be used as a preprocessor and Gauss-Jordan Elimination is back.

Preprocessor usage

The solver can now be used to preprocess CNF or CNF+XOR instances into a simplified, pure CNF instance. This means you will now be able to use CrypoMiniSat as a preprocessor to your favourite SAT solver. To use CryptoMiniSat in this context, just do:

./cryptominisat5 -p1 input.cnf simplified.cnf
#let's run a different solver to solve the simplified CNF
some_sat_solver simplified.cnf > output
#let's get the final solution
./cryptominisat5 -p2 output

You can also change the global timeout for all the preprocessing stages by setting for example “-m 2.0”, that doubles the timeout for every preprocessing step. You can also change the order of the preprocessing steps. Just pass the option ‘–preschedule “SCHEDULE” ‘ where the default schedule 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

Note that “renumber” is variable re-numbering and you probably want to have at as the very last. You can have any of these inprocessing steps any number of times. The “occ-*” ones should be next to one another as they then share the same occurrence list, reducing the number of times the occurrence list needs to be built.

Gauss-Jordan Elimination

Gaussian elimination is back! It now works with all the inprocessing steps that have been mostly invented by trio of Biere, Heule and Jarvisalo. To use Gauss-Jordan elimination, build the system as:

tar xzvf cryptominisat-5.0.0.tar.gz
cd cryptominisat
mkdir build && cd build
cmake -DUSE_GAUSS=ON ..
make

You will then end up with a cryptominisat5 that has Gauss-Jordan elimination compiled in. It auto-detects whether it’s useful on the CNF passed. In case you know you must use it, pass the option “–autodisablegauss 0” so Gauss-Jordan doesn’t get disabled. If you need more matrixes than default, pass “–maxnummatrixes N”.

Executable Binaries

Static executable binaries have been released for CryptoMiniSat 5.0.0 for both Linux and Windows. It should be easy to build binaries on most platforms though, including OS X, Linux, and Windows. Please see the release page.

Future Work

I plan on incorporating Tero Laitinen’s work so the Gauss-Jordan elimination might get somewhat better. Gauss-Jordan might come pre-compiled in the future with the system. I also plan to incorporate the SAT Competition Main track’s winner idea into mainline CryptoMiniSat. These should come with CryptoMiniSat 5.1.0