CryptoMiniSat v2 finally released

SAT,

CryptoMiniSat version 2.4.0 is finally here. I decided to use the INRIA Gforge system to coordinate bug-hunting, release management and the forums. However, the source code revision management is coordinated through Gitorious. There, you can find all revisions that have been made to CryptoMiniSat since its original SVN revision control was fixed to use trunk and branches. I believe at least a 1000 revisions are up, so you can see how the source evolved. The source now should be pretty stable, but I am looking forward to all bug reports and suggestons.

Gaussian elimination is currently disabled. It is present in the code, however, and can be enabled. The reason for disabling it is that I haven’t used it for quite some while. This means it needs testing to be stable, and some very minor tuning needs to be carried out to make work with the much updated internal state of CryptoMiniSat.

I hope this release is just a starting point for a number of upcoming releases that will be made in a much more transparent manner than they have been done until now. I am looking forward to feature requests, bug report and merge requests both in the Gforge and the Gitorious intefaces. Good SAT solving!

On PrecoSat

SAT,

Lately, I have been having a poll of who will win the SAT Race’10. Apparently, 5 people voted until now, me included. I voted PrecoSat. Not because I didn’t want to vote CryptoMiniSat, but because I honestly believe it really will win. The reason is awfully simple: Armin Biere, the (main) author of PrecoSat has had far more experience and time than me to perfect his solver. This is normal, though I only hope he might notice the amount of effort that was put into CryptoMiniSat.

CryptoMiniSat now contains ~10’000 lines of code, compared to the original so-called ‘core’ MiniSat it has been developed from, which contained ~1’000. A ten-fold increase in code, which represents more than 1300 commits in the main tree (and about 1.5 years of my life). This effort has not been carried out alone. Though I haven’t much talked about people that helped me on the way, CryptoMiniSat has been tested and patches have been committed by a number of people, putting a lot of their time and effort into making a working SAT solver. They all worked just for the fun of being part of the project.

The collaborative nature of the CryptoMiniSat project is partially the reason why, I hope, it might succeed in the end in becoming a viable alternative to PrecoSat. End of next week, I will post the whole revision history of CryptoMiniSat to Gitorious, so everyone can see how certain options evolved over time — my commit messages are usually (overly) long ;) Then, bugzilla, mailing lists, forums and the rest will hopefully garner some steam, and we can start rolling. The road is wide ahead…

Optimisations

SAT, ,

There are plenty of optimisations that I have tried with CryptoMiniSat. I will try to list a few that I finally didn’t consider using, but could be implemented later to get around 4-8% speedup each.

It seems a good idea to use a separate CNF simplifier such as SatELite before executing the SAT solver. The reasoning is, that even though one can import (or copy-paste) the code from SatELite, the memory will stay fragmented: variable elimination might remove half the variables, and so the arrays that store variable values will have unused bytes in them, using a larger footprint than necessary, thus causing cache misses. Though this is true, SatELite is not exactly perfect. For instance, it can be seen in certain instances of the SAT Competition of 2009 that GLUCOSE sometimes had very bad performance in comparison with other solvers exactly because SatELite took, e.g. 130 seconds, but the solving only took 2 seconds. So SatELite slowed down the solving of this instance. Also, SatELite has some limitations, e.g. it cannot handle more than 4’800’000 clauses otherwise it might take just too much time. These are huge drawbacks, and in fact CryptoMiniSat (and, e.g. PrecoSat) overcomes all of these. The memory fragmentation issue remains, though. It could be treated, but that would require about 2-3 weeks of time to get corrected, and I simply don’t have that much time. P.S.: Easy solution: rename the variables everywhere. Hard (but less error-prone) solution: use different datastructure for variable values.

Another possible optimisation that never made it to CryptoMiniSat (though I have a branch in git that achieves it more-or-less) is the close packing of clauses in memory. It can greatly increase the cache-hit ratio, though only for relatively small (<20-40 MByte) problems. The reason why I never got this done is that it is a source of a lot of potential problems. Firstly, there is no point in packing clause sizes that are rare. The most common clause size is 2 (see SAT Competition instances), so it’s only logical to pack these clauses. However, this presents a problem: how should the clause be freed after usage? If it was a packed clause, it needs to be freed specially (from the packed heap). But sometimes, non-packed clauses shrink to size 2, so they should become packed. Must these clauses be freed, and then re-allocated from the packed heap? Doesn’t that add too much complexity? Also, according to my experience, packed heaps only help when the problem is small. For large problems, the cache miss rate will be very high anyway, and so packing won’t make much of a difference.

There are some other optimisations that I missed out on, I think. I will one day look through my very messy git tree (with 41 branches and approx. 1600 commits) to see which ones did I once implement and never got working :)

PS: After the start of the SAT Race 2010, I will put all of the git tree up into gitorious. Then, everyone can use it and try to merge these trees into the main tree, and see what happens.

Tools that I often use

Personal,

I used to use Perl a lot in the old days. Martin Albrecht, through the sage mathematics software, showed me Python. I first really hated Python. But then, I realised I can simply type away in it, as in C++, but without all the hassle of C++. I saw a little of AWK once, and I got madly in love with it — when it comes to simple scripts like counting numbers printed by programs, AWK is unbeatable. I use grep a lot, and recently I realised how great a combination grep and wc (a very dumb utility that counts lines/words) are. For instance, I can simply do: “grep “s SAT” *.output | wc -l” to find how many problems have been solved by CryptoMiniSat. I am also finding myself using grep and AWK together to create shell scripts that I run later. For example, I can do: “ls *.cnf | awk ‘{print “./cryptominisat ” $1 ” > ” $1.output” }’ > script.sh” which, when executed, solves all CNF files in the directory, and generates a *.cnf.output file for each, containing the output of CryptoMiniSat. An interesting utility in UNIX is ulimit, with which can limit the memory and time (and stack, etc.) usage of a process. Putting a “ulimit -t 10000” at the beginning of our “script.sh” we can simply limit CryptoMiniSat to 10000 seconds for each instance.

As for failures in terms of the tools I use, I can probably list a few. I tried very hard to learn Haskell, a purely functional language, but I simply couldn’t fully wrap my head around it. Haskell bothered me, because it seems so intuitive, yet it is so hard to master. I haven’t yet got around learning sage, either, even though I think Martin Albrecht is doing a great service to the community by coordinating it. I hope one day CryptoMiniSat will be used inside it, though :)

My connection with the boost library is a love-hate relationship. I think boost is just amazing: it lets me program with the least amount of effort, creating a program that is less error-prone, more robust and multi-platform. However, at the same time, many programmers avoid it like the plague, for multiple reasons. Firstly, the library changes so often that something you wrote just two months ago might not compile with the new boost. Secondly, it’s a nuisance to have dependencies in the code. Thirdly, compilation times can increase significantly e.g. with the Spirit parser. I don’t agree with the second argument, since boost as a dependency isn’t significant and it saves on a lot of debugging time, and the third argument is becoming moot due to gcc 4.5. But the first argument has, actually, hit me too, and it is very unpleasant.

216

SAT,

216. I am quite proud of this number. It’s the number of instances CryptoMiniSat2 can solve from the 292 problem instances of the SAT Race’09, given roughly the same amount of time and computing resources as the solvers of 2009. Last year’s winner could solve only 204. Total solving time of CryptoMiniSat for the 216 instances was 217’814 sec, in comparison to 180’345 sec (for 12 less instances) of last year’s winner. The distribution of SAT and UNSAT for CryptoMiniSat is 85 SAT and 131 UNSAT instances solved. With this performance, it would have won all three tracks of the competition (SAT, UNSAT and SAT+UNSAT) last year.

Of course, this performance doesn’t mean much in terms of the 2010 SAT Race. I would like to have CryptoMiniSat be in the top three, but who knows what other solvers are capable of. Also, I only tested on these 292 instances — there could be some grave bugs and regressions on other types of instances. I will try to test on a larger number of instances, just to see if there are some grave regressions, but I am not very good at finding bugs. However, the STP team has been great at finding bugs: they have found 3 major ones until now. Unfortunately, I am convinced there are many more.

What bugs me the most about CryptoMiniSat is that I am totally incapable of doing AIG (And-Inverter Graphs). It seems great, and some good researchers of SAT (e.g. Armin Biere, Niklas Een) are proficient in it — but to me it’s completely impenetrable. I wanted to buy a book from Amazon on Electronic Design Automation, and I wanted to read through all what Biere wrote on this topic, but I need someone to guide me. However, I simply don’t know anyone in person who knows AIG. My ignorance of AIG is a real shame, and I just feel like being stupid. I really do.