All posts by msoos

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.

A great essay on security in the cyberworld

Personal,

I just read this paper on cybersecurity by Daniel E. Geer, and I was very impressed. Unfortunately I haven’t heard from the author yet, but I regularly used to read the blog of Bruce Schneier, and this essay basically puts the same ideas into perspective.

I have found the essay to be very interesting, and very thought-provoking. It shows very well that security in the cyber (or cyber-connected) world is very difficult to attain. There are no simple solutions. I personally think that security in the real world (not only the cyber world) is also very difficult to obtain, and unfortunately politicians tend to go the easy way, and simply bend in front of the will of the people by implementing “security measures” that in the end don’t help much (if at all) in terms of security, but reassure the people. An example of this is the ban of liquids on airplanes, while cockpits in Europe are still not reinforced — the former doesn’t achieve much but is very visible (and so is more of a security theater), while the latter would be much less visible, but also much more effective. Also to note, that the former takes a lot of man-power to implement, and inconveniences the users (thus taking their time, too), while the latter would be relatively cheap.

The mentality that leads us to believe that bombing is more of a threat is that most people expect planes to be blown up, while hijacking is most only an afterthought. This serious mistake is probably a psychological effect, as most people tend to remember visually colourful incidents more, and Hollywood has made use of the “blow-up” effect too much, etching it into the brains of most people, even decision-makers. However, it is important to remember, that most serious problems in airports and airplanes were carried out through the use of arms other than bombs: to take a trivial example, no planes used in 9/11 were bombed. As a side-note, reinforced cockpits would have prevented all of 9/11, and European cockpits are still not reinforced, but my toothpaste is always taken away — a serious defect, I say.

The dates of the SAT Race 2010 have been announced!

SAT

The dates of the SAT Race 2010 have been announced! The deadline is the end of April, so I have to get CryptoMiniSat bug-free by then.

I have decided to merge the code into STP, the Simple Theorem Prover made by some MIT researchers, among them Vijay Ganesh, with whom I have have worked quite a lot during the final months of 2009. Hopefully, with the help of the STP team, CryptoMiniSat will be bug-free by the end of this month, and through testing in STP, fine-tuning of options will be carried out. There are 16 new modules in the solver, and all have heuristic cut-offs, which have to be tuned. Naturally, I tried to use sensible defaults, but problems can vary widely, and different problems need different cut-offs. For instance, if the number of clauses is very low, even O(m^2) algorithms can be executed, while if the number of clauses is extremely large, e.g. 100’000, it might take too much time even to execute O(m*log(m)) algorithms.

If you are interested in the new CryptoMiniSat, all you need to do is to observe the developments in STP. I will also make the unstable executables accessible from this blog, through links, whenever I have a new version. Fingers crossed for a correct and fast CryptoMiniSat!