Reference:
Matti Järvisalo and Tommi Junttila. Limitations of restricted branching in clause learning. Constraints, 14(3):325–356, 2009.
Abstract:
The techniques for making decisions, that is, branching, play a central role in complete methods for solving structured instances of constraint satisfaction problems (CSPs). In this work we consider branching heuristics in the context of propositional satisfiability (SAT), where CSPs are expressed as propositional formulas. In practice, there are cases when SAT solvers based on the DavisPutnamLogemannLoveland procedure (DPLL) benefit from limiting the set of variables the solver is allowed to branch on to so called input variables which provide a strong unit propagation backdoor set to any SAT instance. Theoretically, however, restricting branching to input variables implies a superpolynomial increase in the length of the optimal proofs for DPLL (without clause learning), and thus inputrestricted DPLL cannot polynomially simulate DPLL. In this paper we settle the case of DPLL with clause learning. Surprisingly, even with unlimited restarts, inputrestricted clause learning DPLL cannot simulate DPLL (even without clause learning). The opposite also holds, and hence DPLL and inputrestricted clause learning DPLL are polynomially incomparable. Additionally, we analyze the effect of inputrestricted branching on clause learning solvers in practice with various structured realworld benchmarks.
Keywords:
propositional satisfiability, branching heuristics, clause learning, DPLL, proof complexity, problem structure, backdoor sets
Suggested BibTeX entry:
@article{JarvisaloJ:Constraints09,
author = {Matti J\"arvisalo and Tommi Junttila},
journal = {Constraints},
number = {3},
pages = {325356},
title = {Limitations of Restricted Branching in Clause Learning},
volume = {14},
year = {2009},
}
