Impact of Restricted Branching on Clause Learning SAT Solving

Reference:

Matti Järvisalo. Impact of restricted branching on clause learning SAT solving. Research Report A107, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, August 2007. ISBN 978-951-22-8907-3.

Abstract:

Propositional satisfiability (SAT) solving procedures (or SAT solvers) are used as efficient back-end search engines in solving industrial-scale problems such as automated planning and verification. Typical SAT solvers are based on the Davis-Putnam-Logemann-Loveland procedure (DPLL), which performs an intelligent depth-first search over the solution space of a propositional logic formula. A key technique in SAT solvers is clause learning, which has been shown to make DPLL more efficient both theoretically and in practice. Branching heuristics, that is, deciding on which variable to next set a value during search, also plays an important role in the efficiency of search.

This report investigates the effect of structure-based branching restrictions on the efficiency of modern DPLL based SAT solvers with clause learning. Branching restrictions force the solver to restrict its decision making to a subset of the problem variables. Ideally, if the branching restriction consists of structurally important variables, the solver is guided to making relevant decisions, decreasing the time needed for solving the problem instance.

The contributions of the report are two-fold. On one hand, a theoretical investigation of the effect of so called input restricted branching on the proof complexity theoretic efficiency of the proof system underlying DPLL based SAT solvers with clause learning is presented. It is shown that with input restricted branching, clause learning DPLL is polynomially incomparable with the standard DPLL. This implies that all implementations of clause learning DPLL, even with optimal heuristics, have the potential of suffering a notable efficiency decrease when input restricted branching is applied.

On the other hand, an extensive experimental evaluation of the effect of different structure-based branching restrictions on the practical efficiency of a state-of-the-art clause learning DPLL implementation is provided. Compared to experimental evaluations found in the literature, the treatment is both deeper and wider: it is not limited to comparing running times and it provides more detailed experimental evidence for the reasons why input restricted branching has the potential of reducing search efficiency. The work also investigates the effect of restricting branching in a controlled way based on structural properties other than the plain input restriction.

Keywords:

Boolean circuits, branching heuristics, clause learning, constraint solving, DPLL, experimentation, problem structure, proof complexity, propositional satisfiability

Suggested BibTeX entry:

@techreport{HUT-TCS-A107,
    address = {Espoo, Finland},
    author = {Matti J\"arvisalo},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {August},
    note = {ISBN 978-951-22-8907-3},
    number = {A107},
    pages = {viii+62},
    title = {Impact of Restricted Branching on Clause Learning {SAT} Solving},
    type = {Research Report},
    year = {2007},
}