Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:
Academic
Publications
Representation and Evaluation of QBFs in Prenex-NNF
Edit
Representation and Evaluation of QBFs in Prenex-NNF  
BibTex | RIS | RefWorks Download
Theoretical and practical investigations have shown that some forms of reasoning such as belief revision, non- monotonic reasoning, reasoning about knowledge, and STRIPS-like planning can be formulated by quantified Boolean formulas (QBFs) and can be solved as instances of quantified satisfiability problem (QSAT). Almost all existing QSAT solvers only accept QBFs represented in prenex-CNF. Formulating problems into QBFs usually does not yield prenex-CNF. Therefore, they are required to transform the obtained formula into prenex-CNF before launching it to a QSAT solver. This task usually cannot be done efficiently. In this paper we show how Zero-Suppressed Binary De- cision Diagram (abbreviated by ZBDD or ZDD) can be used to represent QBFs given in prenex-NNF and evaluate them efficiently. Transforming any QBF into its equivalent in prenex-NNF usually can be done efficiently.
Published in 2004.
Cumulative Annual
Share this on | Contribute to Academic