Propositional Fragments for Knowledge Compilation and Quantified Boolean Formulae

Sylvie Coste-Marquis, Daniel Le Berre, Florian Letombe, Pierre Marquis

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 (quite influential) ordered binary decision diagrams, prime implicates, prime implicants, ``formulae'' in decomposable negation normal form. On the other hand, the validity problem QBF 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 for this purpose. In this paper, the complexity of restrictions of {\sc qbf} obtained by imposing the matrix of the input QBF to belong to such propositional fragments is identified. Both tractability and intractability results (PSPACE-completeness) are obtained.

Content Area: 5. Automated Reasoning

Subjects: 3. Automated Reasoning

Submitted: May 10, 2005

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.