DPLL and resolution are two popular methods for solving the problem of propositional satisfiability. Rather than algorithms, they are families of algorithms, as their behavior depends on some choices they face during execution: DPLL depends on the choice of the literal to branch on; resolution depends on the choice of the pair of clauses to resolve at each step. The complexity of making the optimal choice is analyzed in this article. Extending previous results, we prove that choosing the optimal literal to branch on in DPLL is Delta(p)(2)[logn]-hard, and becomes NPPP-hard if branching is only allowed on a subset of variables. Optimal choice in regular resolution is both NP-hard and coNP-hard. The problem of determining the size of the optimal proofs is also analyzed: it is coNP-hard for DPLL, and Delta(p)(2)[logn]-hard if a conjecture we make is true. This problem is coNP-hard for regular resolution.

Complexity results on DPLL and resolution / Liberatore, Paolo. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - STAMPA. - 7:1(2006), pp. 84-107. [10.1145/1119439.1119442]

Complexity results on DPLL and resolution

LIBERATORE, Paolo
2006

Abstract

DPLL and resolution are two popular methods for solving the problem of propositional satisfiability. Rather than algorithms, they are families of algorithms, as their behavior depends on some choices they face during execution: DPLL depends on the choice of the literal to branch on; resolution depends on the choice of the pair of clauses to resolve at each step. The complexity of making the optimal choice is analyzed in this article. Extending previous results, we prove that choosing the optimal literal to branch on in DPLL is Delta(p)(2)[logn]-hard, and becomes NPPP-hard if branching is only allowed on a subset of variables. Optimal choice in regular resolution is both NP-hard and coNP-hard. The problem of determining the size of the optimal proofs is also analyzed: it is coNP-hard for DPLL, and Delta(p)(2)[logn]-hard if a conjecture we make is true. This problem is coNP-hard for regular resolution.
algorithms; automated reasoning; computational complexity; davis-putnam; np-completeness; performance; propositional satisfiability
01 Pubblicazione su rivista::01a Articolo in rivista
Complexity results on DPLL and resolution / Liberatore, Paolo. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - STAMPA. - 7:1(2006), pp. 84-107. [10.1145/1119439.1119442]
File allegati a questo prodotto
File Dimensione Formato  
VE_2006_11573-125447.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 262.52 kB
Formato Adobe PDF
262.52 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/125447
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact