You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Complexity Results for Quantified Boolean Formulae Based on Complete Propositional Languages1

Article type: Research Article

Authors: Coste-Marquis, Sylvie | Le Berre, Daniel | Letombe, Florian | Marquis, Pierre

Affiliations: CRIL/CNRS, Université d’Artois, rue de l’Université — S.P. 16, F-62307 Lens, France. E-mails: coste@cril.univ-artois.fr, leberre@cril.univ-artois.fr, letombe@cril.univ-artois.fr, marquis@cril.univ-artois.fr

Note: [1] A preliminary version of this paper appeared in the proceedings of the 20th National Conference on Artificial Intelligence (AAAI’05), pp. 288–293.

Keywords: automated reasoning, quantified Boolean formulae

DOI: 10.3233/SAT190003

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 1, no. 1, pp. 61-88, 2006

Received 1 September 2005
|
Revision received 1 March 2006
|
Published: 1 March 2006
Get PDF open access

Abstract

Several propositional fragments have been considered so far as target languages for knowledge compilation and used for improving computational tasks from major AI areas (like inference, diagnosis and planning); among them are the ordered binary decision diagrams, prime implicates, prime implicants, “formulae” in decomposable negation normal form. On the other hand, the validity problem val(QPROPPS) for Quantified Boolean Formulae (QBF) has been acknowledged for the past few years as an important issue for AI, and many solvers have been designed. In this paper, the complexity of restrictions of the validity problem for QBF obtained by imposing the matrix of the input QBF to belong to propositional fragments used as target languages for compilation, is identified. It turns out that this problem remains hard (PSPACE-complete) even under severe restrictions on the matrix of the input. Nevertheless some tractable restrictions are pointed out.

Show less