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. (C) 2000 Elsevier Science B.V. All rights reserved.
On the complexity of choosing the branching literal in DPLL / Liberatore, Paolo. - In: ARTIFICIAL INTELLIGENCE. - ISSN 0004-3702. - STAMPA. - 116:1-2(2000), pp. 315-326. [10.1016/s0004-3702(99)00097-1]
On the complexity of choosing the branching literal in DPLL
LIBERATORE, Paolo
2000
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. (C) 2000 Elsevier Science B.V. All rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
