DIMACS TR: 96-38

How good are branching rules in DPLL?

Author: Ming Ouyang


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.

Paper Available at: ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1996/96-38.ps.gz
DIMACS Home Page