The subtitle of this post should really say: and I was wrong, again. First, let me explain what I have been wrong about — wrong assumptions are always the most instructive.

I have been convinced for the past year that it’s best to have two type of restart and corresponding learnt clause usefulness strategies: the glue-based restart&garbage collection of Glucose and a variation of the geometric restart and activity-based garbage collection of MiniSat. The glue-based variation was observed to be very good for industrial instances with many variables, many of which can be fixed easily, and the MiniSat-type variation was observed to be good for cryptography-type instances with typically low number of variables, almost none of which can be fixed. However, I had the chance to talk to Armin Biere a couple of weeks ago, and while talking with him, I have realised that maybe one of Lingeling’s advantages was its very interesting single restart strategy, based on agility (presentation, PDF) which seemed to let it use glue-based garbage collection all the time, succeeding to solve both types of instances. So, inspired by the CCC crowd, in only 10 minutes I have implemented a simple version of this restart strategy into CryptoMiniSat, and voilá, it seems to work on both type of instances, using only glues!

Now that this dumb assumption of mine is out of the way, let me talk about what is really interesting. As per my last post, I have managed to add a lightweight form of Extended Resolution (ER). Since then, I have improved the heuristics here-and-there, and I have launched the solver on a somewhat strange problem (aloul-chnl11-13.cnf) that only has 2×130 variables, but seems to be hard: very few SAT solvers were able to solve this instance within 10000 secs during the last SAT Competition. So, after CryptoMiniSat cutting the problem into two distinct parts, each containing 130 variables, it started adding variables to better express the learnt clauses… and the average learnt clause size dropped from ~30 literals to ~13 literals in comparison with the version that didn’t add variables. Furthermore, and this is the really interesting part, the solver was able to prove that some of these newly introduced variables must have a certain value, or that some of them were equi- or antivalent to others. So, after lightening the problem up to contain ~3000 variables, the solver was able to solve it in less than 5 minutes. This is, by the way, a problem that neither the newest MiniSat, nor Lingeling, nor Glucose can solve. Interestingly, the Extended Resolution version of Glucose can solve it, in almost the same time as CryptoMiniSat with ER added…