Conflict-based Selection of Branching Rules in SAT-Algorithms.
Marc Herbstritt, Bernd Becker · 2003
The problem of proving that a propositional boolean formula is satisfiable (SAT) is one of the fundamental problems in computer science. The application of SAT solvers in VLSI CAD has become of major interest. The most popular SAT algorithms are based on the well known Davis-Putnam procedure. There, to guide the search, a branching rule is applied for selecting and assigning unassigned variables. Additionally, conflict analysis methods are available that result in non-chronological backtracking that prevents the SAT algorithm from searching nonrelevant parts of the search space. In this paper we focus on the impact of different branching rules and present an approach which (1) allows the use of several branching rules to be applied (not limited to one static rule) and (2) uses information from non-chronological backtracking to dynamically adapt the probabilities of the branching rules to be selected. Our approach results in a faster and more robust behaviour of the SAT algorithm. 1