Limitations of Restricted Branching in Clause Learning

Reference:

Matti Järvisalo and Tommi Junttila. Limitations of restricted branching in clause learning. In Christian Bessiere, editor, Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming (CP 2007), volume 4741 of Lecture Notes in Computer Science, pages 348–363. Springer, 2007.

Abstract:

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 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 analyse the effect of input-restricted branching on clause learning solvers in practice with various structural real-world benchmarks.

Suggested BibTeX entry:

@inproceedings{JarvisaloJ:CP07,
    author = {Matti J\"arvisalo and Tommi Junttila},
    booktitle = {Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming (CP 2007)},
    editor = {Christian Bessiere},
    pages = {348--363},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Limitations of Restricted Branching in Clause Learning},
    volume = {4741},
    year = {2007},
}

See www.tcs.hut.fi ...