After a long break, CryptoMiniSat 2.9.0 has finally been released. The Windows executables need this to work, and the Linux binaries need a recent (>=2.6.26) kernel version. The program has evolved substantially since the last release — more than half of its codebase has been changed. It now works in multi-threaded mode, and uses lazy cached implications for all sorts of interesting purposes from simple transitive on-the-fly self-subsuming resolution to very efficient literal dependency analysis. Currently, the program solves ~225 problems from the 2009 SAT Competition examples given the same time and similar computing power. This is a nice improvement over other SAT solvers such as MiniSat (205), PrecoSat (210) or lingeling (207).

Intensive testing has been carried out on this version of the program, to the extent of finding and identifying a new and unknown gcc bug affecting all gcc versions 4.5.0 and later. Many have played part in finding this and other bugs, including, but not limited to, Martin Maurer, Vegard Nossum, Oliver Kullmann, Robert Aston, and others. This release has been made possible thanks to them.

I hope this version of the code will be useful to many, not only end users but also researchers. In fact I decided to release this version (relatively) early to let researchers merge their changes for the upcoming SAT Competition 2011. I am very interested in any and all versions of CryptoMiniSat that will be submitted to the competition. In case you personally want to change it and find something difficult to understand, just drop a mail to the nowadays very active development mailing list. With this release, I can confidently say that CryptoMiniSat is becoming not only a programming project but also a community. If you feel like you could contribute, or you are simply interested in what is going on, join us.

As for the technical details, the new CryptoMiniSat uses OpenMP for mutli-threading which means it is fully platform-independent. During multi-threading we share unitary and binary clauses between threads — the latter is checked for redundancy using lazy cached implications. We use implicit binary clauses, which don’t help as much in terms of memory as I have hoped, but they help immensely for certain operations, in particular with subsumption checks. Literal dependencies are now calculated using the lazy cached implications and the dominating literal with the largest tree is selected as dominant literal for all literals: when picking variables, we pick the dominating literal 50% of the time instead of the original literal. Variable elimination heuristics have also been highly tuned thanks to the much better at-hand statistics due to implicit binary clauses.

Unfortunately, this version doesn’t offer all the things I wanted it to offer: multi-threaded library interface, extended resolution, distributed solving through MPI, unified restart strategy, and others. All of these (except MPI), and more are however available from the public GIT repository. They work relatively stable, but have a terrible speed: the version with all of these only solves ~214 problems from those above. Therefore, I will personally submit version 2.9.0 to the SAT Competition unless some grave bug is found inside. I might also submit a corrected version of the upcoming 3.0.0 release as well, but as it usually takes a month to tune the solver, and I am currently very busy with some great projects at my new workplace, so a 3.0.0 version probably won’t happen until the deadline.

I hope you will enjoy this new version of CryptoMiniSat! In case of questions, problems or bugs, please contact either me, or the development mailing list and join in to collaborate :)