On the complexity of choosing the branching literal in DPLL

Artificial Intelligence

In this paper we analyze a computational problem raising from the well-known DPLL algorithm for checking satisfiability of propositional formulae. The DPLL algorithm is a backtracking algorithm enhanced with three rules to improve efficency. We study the computational complexity of determining whether a variable leads to an optimal search tree, when it is chosen as the branching literal.

 @article{libe-00-a,
 title = {On the complexity of choosing the branching literal in DPLL},
 year = {2000},
 author = {Liberatore, Paolo},
 journal = {Artificial Intelligence},
 pages = {315-326},
 number = {1-2},
 volume = {116},
 }