It has been a long and winding road, but finally, CryptoMiniSat 2.7.1 has been released. The main additions relative to version 2.6.0 are:

• Lots of documentation. I have added ~1’500 lines of comments to aid developers and user alike
• Transitive on-the-fly self-subsuming resolution — an optimisation I have blogged about
• Memory allocator has been fixed and updated
• DIMACS parsing is now much better, which should allow for very interesting usage scenarios

Although the above list doesn’t seem to talk about performance, let me talk about it first. My personal point of view on performance is that different applications have different needs, so even if overall some solver is the best, it might not mean that it is the best for a particular application. I compared the performance of CryptoMiniSat 2.7.1 to the other mainline solvers, namely MiniSat 2.2, PrecoSat465, and lingeling. I ran the problem instances of the 2009 SAT Competition, with a timeout of 6’000 seconds on some powerful computers. The results are the following:

CryptoMiniSat could solve 225 problem instances (223 within SATComp’09 limits), and the second best solver, lingeling, could solve 211 (207 within SATComp’09 limits). Interestingly, both MiniSat 2.2 and lingeling were better than CryptoMiniSat 2.7.1 at low timeouts, and lingeling kept this advantage the longest, until ~500 seconds, above which CryptoMiniSat took over. Not being too fast at the beginning is a conscious choice by me, as I think it helps in the long run, though I might be wrong. There is much to be improved, and I hope that the immense amount of documentation added will help those willing to try to iron out these shortcomings.

As for the DIMACS parsing update, it basically allows to add information to clauses to distinguish between learnt and non-learnt clauses. This helps, because it is now possible to simply dump the learnt clauses at any moment during the search, and then re-start the search more-or-less where it was stopped. The command-line options for this are “–dumplearnts=FILENAME –maxdumplearnts=3” to dump, and “–alsoread=FILENAME” to re-read. This is currently quite a crude way of stopping-and-starting, but hopefully it will improve in the future.

All in all, I am quite happy about the new release. I have put lots of time into it, and I hope you will enjoy using it :)