Solving QBF with counterexample guided refinement

We propose two novel approaches for using Counterexample- Guided Abstraction Re nement (CEGAR) in Quanti ed Boolean Formula (QBF) solvers. The rst approach develops a recursive algorithm whose search is driven by CEGAR (rather than by DPLL). The second approach employs CEGAR as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of families in the QBF-LIB and that the DPLL solver bene ts from the additional type of learning. Thus this article opens two promising avenues in QBF: CEGAR-driven solvers as an alternative to existing approaches and a novel type of learning in DPLL.