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. Many solvers, for example, restart once every k conflicts with such a diverse choice of k as to give the impression that one policy may be just as good as another. 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 this paper we provide strong evidence that the restart policy matters, and deserves to be chosen less arbitrarily, for a clause learning SAT solver. We begin by pointing out that other things held constant, it is the combination of the restart policy and decision heuristic that completely determines 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.
Subjects: 15.7 Search
Submitted: May 13, 2006