Abstraction-Based Algorithm for 2QBF

Mikoláš Janota (joint work with Joao Marques-Silva)

I will present a novel algorithm for deciding the validity of quantified Boolean formulas (QBF) with 2 levels of quantifiers (2QBF). In contrast to existing algorithms, the presented one hinges on counterexample guided abstraction refinement (CEGAR).

QBFs are of interest as they enable a standard representation of PSPACE problems. In particular, 2QBFs enable representing problems in the second level of the polynomial hierarchy. Hence, the presented CEGAR approach provides an alternative to existing algorithms for 2QBF validity and, by extension, to solving decision problems in the second level of polynomial hierarchy.

In addition, I will discuss some properties of the algorithm and present experimental results obtained by comparing its implementation to state-of-the art solvers.