The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study

The techniques for making decisions (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 can determine satisfiability faster if branching in the solver is restricted to a subset of the variables at hand. The underlying idea in these approaches is to prune the search space substantially by restricting branching to strong backdoor sets of variables which guarantee completeness of the search. In this paper we present an extensive experimental evaluation of the effects of structure-based branching restrictions on the efficiency of solving structural SAT instances. Previous work is extended in a number of ways. We study state-of-the-art solver techniques, including clause learning and related heuristics. We provide a thorough analysis of the effect of branching restrictions on the inner workings of the solver, going deeper than merely measuring the solution time. Extending previous studies which have focused on input-restricted branching, we also consider relaxed branching restrictions that are based on underlying structural properties of the variables.