Submitter: Leander Tentrup
Description: Devised by L. Tentrup and M. N. Rabe, is a CEGAR-based algorithm for QBF. The algorithm builds on a decomposition of QBFs into a sequence of propositional formulas called clausal abstraction. Each of the propositional formulas contains the variables of just one quantifier level and additional variables describing the interaction with adjacent quantifier levels.
It uses PICOSAT as back-end SAT solver and BLOQQER as preprocessor.
Details are available in
Rabe, M.N., Tentrup, L.: CAQE: A Certifying QBF Solver. In: Proceedings of the 15th Conference on Formal Methods in Computer-aided Design (FMCAD’15).