Unrestricted Backtracking Algorithms for Satisfiability

This paper proposes a general framework for implementing backtracking search strategies in Propositional Satisfiability (SAT) algorithms, that is referred to as unrestricted backtracking. Different organizations of unrestricted backtracking yield well-known backtracking search strategies. Moreover, this general framework allows devising new backtracking strategies. For example, we propose a stochastic systematic search algorithm for SAT, that randomizes both the variable selection and the backtracking steps of the algorithm. In addition, we illustrate how unrestricted backtracking can be used to develop informed search restart strategies, that only eliminate variable selections that are deemed relevant for the set of conicts identified prior to each restart. Finally, experimental results provide empirical evidence that dierent organizations of unrestricted backtracking can result in competitive approaches for solving hard real-world instances of SAT.