On the complexity of choosing the branching literal in DPLL

24Citations
Citations of this article
16Readers
Mendeley users who have this article in their library.

Abstract

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.

Cite

CITATION STYLE

APA

Liberatore, P. (2000). On the complexity of choosing the branching literal in DPLL. Artificial Intelligence, 116(1–2), 315–326. https://doi.org/10.1016/S0004-3702(99)00097-1

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free