3 ms·
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 algor
by 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.