The effect of restarts on the efficiency of clause learning

Given the common use of restarts in today's clause learning SAT solvers, the task of choosing a good restart policy appears to have attracted remarkably little interest. On the other hand, results have been reported on the use of different restart policies for combinatorial search algorithms. Such results are not directly applicable to clause learning SAT solvers, as the latter are now understood as performing a form of resolution, something fundamentally different from search (in the sense of backtracking search for satisfying assignments). In this paper we provide strong evidence that a clause learning SAT solver could benefit substantially from a carefully designed restart policy (which may not yet be available). We begin by pointing out that the restart policy works together with other aspects of a SAT solver in determining the sequence of resolution steps performed by the solver, and hence its efficiency. In this spirit we implement a prototype clause learning SAT solver that facilitates restarts at arbitrary points, and conduct experiments on an extensive set of industrial benchmarks using various restart policies, including those used by well-known SAT solvers as well as a universal policy proposed in 1993 by Luby et al. The results indicate a substantial impact of the restart policy on the efficiency of the solver, and provide motivation for the design of better restart policies, particularly dynamic ones.