Submitter: Leander Tentrup
Description: Devised by L. Tentrup, is a certifying QBF solver based on a CEGAR-based abstraction algorithm for Prenex non-CNF formulas in QCIR format. It uses MINISAT as back-end solver.
Details are available in
Tentrup, L.: Non-prenex QBF Solving Using Abstraction. In: International Conference on Theory and Applications of Satisfiability Testing, Springer (2016) 393401