(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) t

(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.