An Alternative Representation for QBF

Quantified Boolean formulas are a powerful representation that have been used to capture and solve a variety of problems in Artificial Intelligence. While most research has focused on quantified Boolean formulas in prenex normal form (QBF), we explore an alternative representation of quantified Boolean formulas, called Constrained Quantified Formulas (CQF). CQF allows for a more direct representation of many applications. We present complexity results for CQF and for several subclasses of CQF. We have developed a solver, called QRSsat3, for CQF instances at the second level of the polynomial hierarchy. Computational results of QRSsat3 are compared with the results of solvers for quantified Boolean formulas in prenex normal form.

• Type: Journal
• Year: 2009
• Where: ICAI
• Authors: Anja Remshagen, Klaus Truemper
• Keywords: Artificial Intelligence, Boolean Formulas, CQF Instances, ICAI 2009, Prenex Normal Form