@inproceedings{
    Jarvisalo:RCRA07,
    author = {J\"arvisalo, Matti},
    ps = "jarvisalo.rcra07.ps",
    optseries = "",
    title = "The Effect of Structural Branching on the Efficiency of Clause Learning {SAT} Solving",
    booktitle = "14th RCRA Workshop: Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion",
    optpublisher = "",
    abstract = "The techniques for making decisions, i.e., branching, play a central role in complete methods for solving structured instances of propositional satisfiability (SAT). Experimental case studies in specific problem domains have shown that in, some cases, SAT solvers benefit from structure-based limitations on which variables the solver is allowed to branch. Mainly, the focus has been on input (or independent) variables. Moreover, existing literature sheds little light on the effect of the restriction to the inner workings of SAT solvers, and in many cases current state-of-the-art solver techniques are not used. In this paper we present an extensive experimental evaluation on the effect of structure-based branching restrictions on the efficiency of solving structural SAT instances. The emphasis is on the interplay of structure-based branching restrictions and clause learning based search techniques found in most modern complete SAT solvers: (i) We investigate the effect of input-branching on the effectiveness of clause learning bound heuristics and conflict clauses. (ii) To study whether the robustness of input-restricted branching can be improved, we apply controlled schemes for allowing branching additionally on CNF variables other than inputs based on structural properties---such as the number of occurrences of sub-formulas---of non-clausal formulas.",
    note = "See \url{http://pst.istc.cnr.it/RCRA07/program.html}",
    optpages = "",
    flags = "ACPT public",
    year = "2007",
    pdf = "jarvisalo.rcra07.pdf",
    opteditor = ""
}