How good are branching rules in DPLL?

AbstractThe Davis-Putnam-Logemann-Loveland algorithm is one of the most popular algorithms for solving the satisfiability problem. Its efficiency depends on its choice of a branching rule. We construct a sequence of instances of the satisfiability problem that fools a variety of “sensible” branching rules in the following sense: when the instance has n variables, each of the “sensible” branching rules brings about Ω(2n5) recursive calls of the Davis-Putnam-Logemann-Loveland algorithm, even though only O(1) such calls are necessary