Tag Archives: SAT Race

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!

CryptoMiniSat v2

SAT

Lately, I have been working a lot with CryptoMiniSat, to get it up and running for the 2010 SAT Race, held by Carsten Sinz. Getting CryptoMiniSat fast and bug-free has been a long and winding road. I can now understand the difficulty of choosing magic parameters that these SAT solvers make use of regularly. As I have added ~6000 lines of code to a codebase of ~1500, you can probably imagine the number of magic constants that I had to come up with. Worst of all, these constants interact in non-intuitive and sometimes in a fully “magical” manner.

To test my choice of magic constants, I have been running experiments on the Gird5000 project of French universities. It is quite easy to get access to Grid5000 if you work in a French university, and it is surprisingly easy to run experiments. On the other hand, interpreting the results of such experiments is not so easy :) However, CryptoMiniSat is coming along. On crypto examples I think we are unbeatable. When it comes to other examples, we are good, but we will see how the new MiniSat (yes, it’s coming!) and precosat will do. Apparently, the GLUCOSE people are also planning to enter the competition, so the race will be very interesting. Fingers are crossed that CryptoMiniSat will finish somewhere in the top 3 :)

There are some “secret” improvements that I have made the past couple of months, and there are some open secrets. I tried to incorporate the GLUCOSE restart heuristic, and XORs are automatically detected (XOR clauses are no longer neccessary, but they are of course supported!). This means that CryptoMiniSat is now a plug-and-play experience for all the crypto-folks. I have tested the solver with a good number of crypto problems, and the speedup relative to MiniSat is on the order of 2-50x, depending on the problem.

The new CryptoMiniSat will be released when the SAT Race starts and everyone’s executables have been freezed. I will then detail all the new features. Until then, let me just run a couple of more experiments on that cluster :)