Abstract
Quantified Boolean Formulas (QBFs) enable standard representation of PSPACE problems. In particular, formulas with two quantifier levels (2QBFs) enable representing problems in the second level of the polynomial hierarchy (Π2P, ∑2P). This paper proposes an algorithm for solving 2QBF satisfiability by counterexample guided abstraction refinement (CEGAR). This represents an alternative approach to 2QBF satisfiability and, by extension, to solving decision problems in the second level of polynomial hierarchy. In addition, the paper presents a comparison of a prototype implementing the presented algorithm to state of the art QBF solvers, showing that a larger set of instances is solved. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Janota, M., & Marques-Silva, J. (2011). Abstraction-based algorithm for 2QBF. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6695 LNCS, pp. 230–244). https://doi.org/10.1007/978-3-642-21581-0_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
