On the complexity of choosing the branching literal in DPLL

Paolo Liberatore

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},
 }
 
HTTP download.
doi: 10.1016/S0004-3702(99)00097-1