Limitations of Restricted Branching in Clause Learning

10 years 7 months ago
Limitations of Restricted Branching in Clause Learning
The techniques for making decisions, i.e., branching, play a central role in complete methods for solving structured CSP instances. In practice, there are cases when SAT solvers benefit from limiting the set of variables the solver is allowed to branch on to so called input variables. 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 inputrestricted 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 analyse the effect of input-restricted branching on clause learning solvers in practice with various structural real-world benchmarks.
Matti Järvisalo, Tommi A. Junttila
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CP
Authors Matti Järvisalo, Tommi A. Junttila
Comments (0)