Complete unrestricted backtracking algorithms for Satisfiability
Inês Lynce, João P. Marques-Silva · ePrints Soton (University of Southampton) · 2002
In recent years, different backtrack search Propositional Satisfiability (SAT) algorithms have proposed relaxing the identification of the backtrack point in the search tree. Even though relaxing the identification of the backtrack point can be significant in solving hard instances of SAT, it is also true that the resulting algorithms may no longer be complete. This paper proposes a new backtrack search strategy, unrestricted backtracking, that naturally captures relaxations of the identification of the backtrack point in the search tree, most notably search restarts and random backtracking. Moreover, the paper proposes a number of conditions that guarantee the completeness of generic unrestricted backtracking SAT algorithms.