Solving QBF by Counterexample-Guided Abstraction Refinement

Quantified Boolean formulas (QBFs), as a PSPACE-complete problem, represent a powerful formalism but also a computational challenge. In this talk we will look at how QBFs can be solved by the counterexample-guided abstraction refinement paradigm (CEGAR). The presented technique expands the formula into a SAT problem and uses a SAT solver in a blackbox-fashion. In the second part of the talk we will look at some theoretical aspects of this algorithm, which let us understand the significant improvements in performance on a number of instances in comparison to traditional CDCL solving. This second part of the talk builds on results from proof theory and circuit complexity and therefore we hope that the talk will be interesting both for practitioners as well as theoretitians.

Date:
Speakers:
Mikolas Janota
Affiliation:
INESC-ID
    • Portrait of Jeff Running

      Jeff Running