SAT Solvers as Smart Search Engines

I really like the post, except for the conflation of brute force search and using recomputation as state restoration.<p>In my opinion, a brute force search algorithm is an algorithm that will explore the whole search space without any intelligent pruning of sub-trees (it will visit every element of the state space). Such an algorithm needs to use a state restoration policy, with three main flavours being saving undo-information (trailing asin SAT-solvers, Knuths dancing links), saving redo-information (in order to do recomputation), and copying (saving whole search states in each node) are all valid and useful. They can also be combined, with adaptive recomputation being quite nice in some cases (leaving copies of the seaerch state every now and then, closer togheter the farther down the tree one is).

The article is spot on. Some finds it counterintuitive that SAT solver often can solve problems with redundant clauses (hence larger problems) faster than minimal ones. But you can find the proof faster if you have appropriate lemmas. Since lemmas can be derived from axioms, strictly speaking, all lemmas are redundant. But they help.<p>Note: the author maintains a state-of-the-art SAT solver.

I am certain not a SAT specialist and it is a very frustrating technology. There is little literature and it is very hard to figure out what it means in concrete cases.<p>But this article is way above all that I read on this subject. Many thanks!<p>Just an example: &quot;<i>Modeling has lots of interesting constraints, one of which I often hear and I am confused by: that it should minimize the number of variables. Given the above, that SAT solvers can be seen at as partial evaluation engines that thrive on the fact that they can partially evaluate and partially backtrack</i>&quot;

It&#x27;s rare that I feel like I&#x27;m exactly the target audience for an article, but this is one of those times. Specifically, the advice on formulation is something I&#x27;ve been wondering about for a while. It&#x27;s nice to have the author of a SAT solver come out and say that extra variables can be useful to the solver. I&#x27;d suspected as much from experience, but I had a nagging doubt that I was wrong.