Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

Problem-Sensitive Restart Heuristics for the DPLL Procedure

  • Autor:

    Carsten Sinz, Markus Iser

  • Quelle:

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

  • Datum: June 2009
  • 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.