CAQE (Clausal Abstraction for Quantifier Elimination) is a solver for quantified Boolean formulas (QBF) based on the CEGAR-based clausal abstraction algorithm.
- QBFEval2018 results: 1st place in prenex CNF track, 3rd in hard instances track.
- QBFEval2017 results: 1st and 2nd place in prenex CNF track, 3rd in 2QBF track, 3rd place in random QBF track.
- QBFEval2016 results: 4th place in prenex CNF track, 2nd place in Evaluate & Certify Track, and 4th place in Random QBF Track.
CAQE: A Certifying QBF Solver.Markus N. Rabe and Leander Tentrup.
On Expansion and Resolution in CEGAR Based QBF Solving.Leander Tentrup.
The latest version of CAQE is available on GitHub.
- CAQE qbfeval 2017 (2017-07-19) binary release without certification
- CAQE version 2 (2016-05-19)
Markus N. Rabe, Leander Tentrup
Copyright © 2015-2016 Saarland University