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 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 analyse the effect of inputrestricted branching on clause learning solvers in practice with various structural realworld 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 = {348363},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Limitations of Restricted Branching in Clause Learning},
volume = {4741},
year = {2007},
}
