|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 MINISAT 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). (2015) 136–143