Complete Restart Strategies Using a Compact Representation of the Explored Search Space

Applying restarts to complete search algorithms for constraint satisfaction is an effective method for improving their expected performance on some difficult problems. An issue with restarts is that completeness can be lost if the algorithm is constantly interrupted in the midst of a search. We propose a general method for called path-recording, which guarantees completeness for restart strategies and requires space linear in the number of restarts and decision variables. An example application in the domain of propositional satisfiability testing is presented.