4 ms·

SAT Solvers as Smart Search Engines

45 points by another 8y ago

JPLeRouzic 8y ago
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. But this article is way above all that I read on this subject. Many thanks! Just an example: "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"
sanxiyn 8y ago
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. Note: the author maintains a state-of-the-art SAT solver.
mzl 8y ago
I really like the post, except for the conflation of brute force search and using recomputation as state restoration. 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).
- zero_k 8y ago
  (author here) Well, those are all valid strategies. In fact, in the original work that introduced CryptoMiniSat, I used state saving (you called this copying) to quickly reset state to an old one. One could also say that polarity caching is in fact saving redo-information (at least to some extent -- to what extent, can debated). The thing is -- I am not a pro at these other strategies and I can't talk about them with the same clarity. At the end of the day, all of these are quite abstract in some way -- there are many design choices to be made and many different designs. I just tried to highlight brute force vs. partial evaluation&backtrack. But of course there are many other comparisons to be made. I'm just conscious that I have neither the time nor the expertise to do these all unfortunately :( I let Knuth do the heavy lifting, doing all the comparisons in his books.
sevensor 8y ago
It's rare that I feel like I'm exactly the target audience for an article, but this is one of those times. Specifically, the advice on formulation is something I've been wondering about for a while. It's nice to have the author of a SAT solver come out and say that extra variables can be useful to the solver. I'd suspected as much from experience, but I had a nagging doubt that I was wrong.

45 points by another 8y ago

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. But this article is way above all that I read on this subject. Many thanks! Just an example: "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"

sanxiyn 8y ago

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. Note: the author maintains a state-of-the-art SAT solver.

mzl 8y ago

I really like the post, except for the conflation of brute force search and using recomputation as state restoration. 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).

zero_k 8y ago
(author here) Well, those are all valid strategies. In fact, in the original work that introduced CryptoMiniSat, I used state saving (you called this copying) to quickly reset state to an old one. One could also say that polarity caching is in fact saving redo-information (at least to some extent -- to what extent, can debated). The thing is -- I am not a pro at these other strategies and I can't talk about them with the same clarity. At the end of the day, all of these are quite abstract in some way -- there are many design choices to be made and many different designs. I just tried to highlight brute force vs. partial evaluation&backtrack. But of course there are many other comparisons to be made. I'm just conscious that I have neither the time nor the expertise to do these all unfortunately :( I let Knuth do the heavy lifting, doing all the comparisons in his books.

sevensor 8y ago

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