Random backtracking in backtrack search algorithms for satisfiability

This paper proposes the utilization of randomized backtracking within complete backtrack search algorithms for propositional satisfiability (SAT). In recent years, randomization has become pervasive in SAT algorithms. Incomplete algorithms for SAT, for example the ones based on local search, often resort to randomization. Complete algorithms also resort to randomization. These include state-of-the-art backtrack search SAT algorithms that often randomize variable selection heuristics. Moreover, it is plain that the introduction of randomization in other components of backtrack search SAT algorithms can potentially yield new competitive search strategies. As a result, we propose a stochastic backtrack search algorithm for SAT, that randomizes both the variable selection and the backtrack steps of the algorithm. In addition, we relate randomized backtracking with a more general form of backtracking, referred to as unrestricted backtracking. Finally, experimental results for different organizations of randomized backtracking are described and compared, providing empirical evidence that the new search algorithm for SAT is a very competitive approach for solving hard real-world instances.