CryptoMiniSat 2

CryptoMiniSat is an LGPL-licensed SAT solver that aims to become a premier SAT solver with all the features and speed of successful SAT solvers, such as MiniSat and PrecoSat. The long-term goals of CryptoMiniSat are to be an efficient sequential, parallel and distributed solver.

CryptoMiniSat 2.5 won the sequential category of the SAT Race 2010. A variation of CryptoMiniSat 2.7.1 won a gold and a silver medal in the parallel category of the 2011 SAT Competition.

Download

All releases are available here. The GIT repository is available on github.

Features

CryptoMiniSat tries to put many useful features of MiniSat 2.0 core, PrecoSat ver 236, and Glucose into one package, adding many new features. A list of non-exhaustive features added is available here. Essentially, it’s a pile of interesting additions that have been individually tested to improve performance, and together work very effectively. I also regularly blog about all features that improve performance or which fail to do so.

Contribute back

We need your help to stress-test the program, and send back your experience, suggestions, and bug reports. The quite active development mailing list is available here (also, see the archives). The bug tracker is available from here. The source tree, along with all development branches is available from gitorious. The solver is meant to be developed in a collaborative manner. All merge requests in Gitorious will be checked and if found useful, committed.

Documentation

The main flowgraph of the program is available here.The sourcecode has been updated to include Doxygen-based online documentation. In case you wish to help, or are interested in some specific parts, please send an email to either me, or, preferably, the development mailing list.

Acknowledgments

Bug-hunting thanks: Martin Maurer (MSVC compilation, learnt-clause dumping), Trevor Hansen (fuzzing), Vegard Nossum(latent bugs), Vijay Ganesh (library-debugging), Jerry James (manpage, cleanup) and lots of other people. The Grid’5000 project has been a great help in trying out many different combinations of parameters. Naturally, great thanks go to my current and past professors and affiliations (BUTE, INRIA Rhone-Alpes, LIP6 UPMC) who have supported me pursuing SAT solving.