Propositional Fragments for Knowledge Compilation and Quantified Boolean Formulae
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 in-ference, diagnosis and planning); among them are the (quite influential) ordered binary decision diagrams, prime impli-cates, prime implicants, “formulae ” in decomposable nega-tion normal form. On the other hand, the validity problem QBF for Quantified Boolean Formulae (QBF) has been ac-knowledged 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 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.
Cite
Text
Coste-Marquis et al. "Propositional Fragments for Knowledge Compilation and Quantified Boolean Formulae." AAAI Conference on Artificial Intelligence, 2005.Markdown
[Coste-Marquis et al. "Propositional Fragments for Knowledge Compilation and Quantified Boolean Formulae." AAAI Conference on Artificial Intelligence, 2005.](https://mlanthology.org/aaai/2005/costemarquis2005aaai-propositional/)BibTeX
@inproceedings{costemarquis2005aaai-propositional,
title = {{Propositional Fragments for Knowledge Compilation and Quantified Boolean Formulae}},
author = {Coste-Marquis, Sylvie and Le Berre, Daniel and Letombe, Florian and Marquis, Pierre},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2005},
pages = {288-293},
url = {https://mlanthology.org/aaai/2005/costemarquis2005aaai-propositional/}
}