CryptoMiniSat is an LGPL-licenced 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. There are solvers that are good at one or the other, e.g. ManySat (parallel) or PSolver (distributed), but we wish to excel at all.
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
The current release is available here. The sources and binaries of all current and past CryptoMiniSat releases can be found here. The GIT repository is available here.
Bugzilla
The bugzilla for CryptoMiniSat is available here. You can file your bugreports and feature requests there, and follow how they get resolved.
News
CryptoMiniSat 2.9.2 has been released. Changelog is the following.
Bugfixes: * Bug in --maxsolutions fixed thanks to Martin Maurer * CalcDefPolars was taking >10% time for certain problems. Fixed thanks to Vegard Nossum * Bug in StateSaver of saving&restoring double to unsigned fixed thanks to Martin Maurer * Cache cleaning is finally fixed * Disabling part-finding as it made us loose 3+ points at SAT Comp'11 * Clauses after empty comments sometimes weren't parsed. Thanks to Remy Delmas for noticing this * Solutions were sometimes incorrect when using --maxsolutions=X * Random variable picking was turned off after a short while. Thanks to Martin Maurer for noticing this * XOR-to-normal clause converting routine was buggy * Failed literal probing's hyper-binary resolution engine was taking too much time * Performance regressions relative to branch that went into SatComp'11 have been worked on * FPU check problem fixed thanks to Jerry James * Printing problems related to multi-threading and startup in Main.cpp fixed. Thanks to Martin Maurer for reporting this. Improvements: * Manpage thanks to Jerry James * We don't exit(-1) any more, instead, whe throw. Thanks to Jerry James for this * Time-limiting in subsumption+strengthening+var-elim was not sufficient * "strengthened" qualifier removed from Clause * Way better subsumption+strengthening with 2- and 3-long clauses. * Cache cleaning
CryptoMiniSat 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.
CryptoMiniSat needs your help!
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.
