On the complexity of choosing the branching literal in DPLL Original Research Article

The DPLL (Davis–Putnam–Logemann–Loveland) algorithm is one of the best-known algorithms for solving the problem of satisfiability of propositional formulas. Its efficiency is affected by the way literals to branch on are chosen. In this paper we analyze the complexity of the problem of choosing an optimal literal. Namely, we prove that this problem is both NP-hard and coNP-hard, and is in PSPACE. We also study its approximability.