Carsten Sinz, Markus Iser

In Proc. of the 12th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2009), pages 356-362, Swansea, UK

Search restarts have shown great potential in speeding up SAT solvers based on the DPLL procedure. However, most restart policies presented so far do not take the problem structure into account. In this paper we present several new problem-sensitive restart heuristics. They all observe different search parameters like conflict level or backtrack level over time and, based on their development, decide whether to perform a restart or not.We also present a Java tool to visualize these search parameters on a given SAT instance over time in order to analyze existing heuristics and develop new one.