@article{JarvisaloJ:Constraints09,
author = {Matti J\"arvisalo and Tommi Junttila},
journal = {Constraints},
number = {3},
pages = {325-356},
title = {Limitations of Restricted Branching in Clause Learning},
volume = {14},
year = {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 Davis-Putnam-Logemann-Loveland
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
super-polynomial increase in the length of the optimal proofs for DPLL
(without clause learning), and thus input-restricted DPLL cannot
polynomially simulate DPLL. In this paper we settle the case of DPLL
with clause learning. Surprisingly, even with unlimited restarts,
input-restricted clause learning DPLL cannot simulate DPLL (even without
clause learning). The opposite also holds, and hence DPLL and
input-restricted clause learning DPLL are polynomially incomparable.
Additionally, we analyze the effect of input-restricted branching on
clause learning solvers in practice with various structured real-world
benchmarks.