Complete Search Restart Strategies for Satisfiability
Luís Baptista, Inês Lynce, João P. Marques-Silva · 2001
Search restarts is a well-known strategy for coping with hard real-world satisfiable (and often unsatisfiable) instances of Propositional Satisfiability (SAT), that is already being used by different state-of-the-art SAT solvers. Despite being extremely effective for solving real-world problem instances, the original search restart strategy yields an incomplete algorithm, that for unsatisfiable instances is unable to guarantee that unsatisfiability can be established. This paper describes different techniques for guaranteeing the completeness of SAT algorithms that implement search restart strategies, and proposes implementation optimizations to some of the proposed techniques. Experimental evidence indicates that the proposed techniques are effective for a wide range of real-world problem instances.