Abstract
We present a detailed description, analysis, and evaluation of the clausal abstraction approach for solving quantified Boolean formulas (QBF). The clausal abstraction algorithm started as a solving algorithm for QBFs in prenex conjunctive normal form (PCNF) incorporating an efficient Skolem and Herbrand function extraction. Extracting witnesses from solving is especially important as it enables the certification of the solver’s verdict and it is the foundation for applications built on QBF, like verification and synthesis. Later, the algorithmic ideas were extended to non-prenex and negation normal form formulas, leading the way for improved performance in solving and function extraction. The implementations of the algorithms in the solvers CAQE and QuAbS won the QBF competition (QBFEVAL’18) in their respective categories, prenex CNF and prenex non-CNF.