Branching Rules for Satisfiability

Recent experience suggests that branching algorithms are among the most attractive for solving propositional satisfiability problems. A key factor in their success is the rule they use to decide on which variable to branch next. We attempt to explain and improve the performance of branching rules with an empirical model-building approach. One model is based on the rationale given for the Jeroslow-Wang rule, variations of which have performed well in recent work. The model is refuted by carefully designed computational experiments. A second model explains the success of the Jeroslow-Wang rule, makes other predictions confirmed by experiment, and leads to the design of branching rules that are clearly superior to Jeroslow-Wang.