Category Archives: SAT

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.

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.

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!

On research in general

Personal, SAT

I am not sure I am qualified to talk about research in general, but I will try to do my best.

To me, it seems that the research community of any given topic is pretty small. The reason for this is many-fold. Firstly, I suspect that the number of qualified individuals willing to work for a relatively small pay (but with many benefits, like flexible schedule, less stress, etc.) is relatively small. Secondly, any given topic usually reaches a maturity level where the subdomains are very clear, and it is very difficult to say anything reasonably good about a subdomain that one is not acquainted with. For instance, Knuth’s books are brilliant, but even he (someone who is like a semi-god in computer science) acknowledges that he simply cannot be an authority on all the topics covered in the 4th volume of his series. (BTW I just bought Vol4F0 and Vol4F1, wainting for amazon to ship now).

Since the research community is small, everyone gets to know one another. This is great since it helps collaboration, but it also might backlash against newcomers (PhD students), and against people generally not well-acquainted with the field, but who genuinely have good ideas that they wish to publish. I guess it’s a difficult integration process, that gets all the more difficult because it rarely happens that someone can simply stay in the same specific subfield for his entire research career. And even if someone stays in the same field, the field may change so much over time, attracting researchers from many distinct research domains, that even an “oldboy” can feel detached from his/her own topic after a while.

Research that deals with practical things is even more fast-moving than other kinds of research. Just a couple of years ago, research on botnets didn’t exist, yet now it seems it is a very rapidly evolving research domain. SAT solvers – I believe – also fall into the category of practical research. Year after year the solvers evolve so much that trying to compare two solvers with only 1-2 years of difference in their release dates seems nonsensical. This is great because there is a lot of “buzz” going on, but at the same time, it feels like a race against time: inspiring at first, but tiring at the end.

Very theoretical domains rarely have this speed of change. For instance, last year at the SAT’09 conference, I saw Stephen Cook, the person who basically invented the notion of NP completeness (I felt honoured just to be in the same room with him, I must say). Although SAT has changed a lot in the past years (many new applications, e.g. cryptography), but the fundamental problem didn’t change – therefore, he never had the ground taken from under him. The ground sure moved, but he still masters it, I am sure.

Oh well, legends. I met Shamir twice. Very kind person. Also, I met Daniel J. Bernstein at EUROCRYPT’09. He looked somewhat shorter and younger than I imagined, and I liked his openness. I met Lenstra at CCC’08. I was so shocked it was him, I couldn’t even say hello – very embarrassing. He was very friendly, and seemed much younger than his official age would suggest. I really want to meet Knuth, but I guess that might have to wait… forever, maybe. Unless I somehow manage to visit Stanford one day, in which case I will definitely show up at one of his classes. They say he is a terrific speaker.

Why CryptoMiniSat can’t use MATLAB to do Gaussian elimination

SAT

Some people, who may not have thought through the problem of implementing Gaussian elimination into SAT solvers, seem to think that it’s just a matter of pulling a matlab function into a solver, and the job is done. Let met explain why I think this is not the case.

Firstly, we don’t wish to execute Gaussian elimination simply before the solving, instead, we wish to execute it during the solving. This means the matrix’s columns need to be changed often, since as we move down the search tree, some variables will be fixed, thus the columns need to be cleared, and the augmented column needs to be updated. But how would a matlab function know which column was changed? These functions are made to work on any given matrix, churn through it, and finish with a result. However, in many cases, the change (=delta) between two matrixes is minimal (i.e. 3rd column from right was changed). In this case, the matlab routine will nevertheless start updating the matrix from the leftmost column, essentially taking far more time than an algorithm that knows that the delta was small.

Secondly, let’s assume that a value like “x1=true” has been found by the matlab function. Since we don’t know where this information came from, there is only one way of adding it: put it into the propagation queue. This, however, would be a grave mistake. By not giving the solver a hint where this propagation came from, the solver cannot use this information during conflict generation, and we will loose most of the benefits. In case a conflict is found by our matlab function, the problem is even worse. What caused the conflict? We simply don’t know. We can send the solver back one decision level, and hope for the best, but non-historical backjumping is one of the main reason SAT solvers perform so well. On the other hand, if we keep another matrix, not assigned with the current assignements but updated with all row-xor and row-swap operations (as in CryptoMiniSat2), then we will have all these informations at our disposal, and the integration of Gaussian elimination into the SAT solving process will be correct.

These two reasons should be sufficient to see that matlab, or really any mathematical package that implements Gaussian elimination is not useful for CryptoMiniSat. Yes, some of their “tricks” could be used, and I think are already being used.

PS: As a side-note, many have told me that the matrixes are sparse, and so I should use a sparse matrix data structure. Although the matrixes are indeed sparse, they are also miniscule. On very small matrixes (<200-300 columns) there is simply no point in doing sparse matrix elimination. Not to mention, that since two different matrixes need to be stored and handled, it is impossible to find a pivot that is optimal for both, thus the density of at least one of the matrixes must evolve faster than optimal, leading to an early switch to a dense matrix representation.