Heuristic-based backtracking for prepositional satisfiability

Abstract

In recent years backtrack search algorithms for Propositional Satisfiability (SAT) have been the subject of dramatic improvements. These improvements allowed SAT solvers to successfully solve instances with thousands of variables and hundreds of thousands of clauses, and also motivated the development of many new challenging problem instances, many of which still too hard for the current generation of SAT solvers. As a result, further improvements to SAT technology are expected to have key consequences in solving hard real-world instances. The objective of this paper is to propose heuristic approaches to the backtrack step of backtrack search SAT solvers, with the goal of increasing the ability of a SAT solver to search different parts of the search space. The proposed heuristics are inspired by the heuristics proposed in recent years for the branching step of SAT solvers, namely VSIDS and some of its improvements. Moreover, the completeness of the new algorithm is guaranteed. The preliminary experimental results are promising, and motivate the integration of heuristic backtracking in state-of-the-art SAT solvers. © Springer-Verlag Berlin Heidelberg 2003.