Solving QBF by Abstraction

Leander Tentrup

Many synthesis and verification approaches rely on solving techniques for quantified Boolean formulas (QBF). Consequently, solution witnesses, i.e., Boolean functions, become more important as they represent implementations or counterexamples. We present a new recursive counterexample guided abstraction refinement algorithm for solving and certifying QBFs that exploits structural reasoning on the formula level. The algorithm decomposes the given QBF into one propositional formula for every scope, a maximal block of consecutive quantifiers of the same type, that abstracts from assignments of outer and inner quantifiers. Further, we define a format for proof traces and present an efficient method to extract certificates from traces that allows building witnessing functions and certifying the solver result. We report on experimental evaluation of this algorithm in a prototype solver QuAbS (Quantified Abstraction Solver) using synthesis benchmark sets and show the effectiveness of the certification approach.