The 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 Omega(2^(n/5))
recursive calls of the Davis-Putnam-Logemann-Loveland algorithm, even
though only O(1) such calls are necessary.
DIMACS Home Page