@inproceedings{
    JarvisaloJ:CP07,
    editor = "Bessiere, Christian",
    author = {J\"arvisalo, Matti and Junttila, Tommi},
    publisher = "Springer",
    title = "Limitations of Restricted Branching in Clause Learning",
    url = "http://www.tcs.hut.fi/~mjj/publications.shtml",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming (CP 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.",
    volume = "4741",
    flags = "ACPT public",
    year = "2007",
    pages = "348--363"
}