CAQE

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.

Paper

[RT15]

CAQE: A Certifying QBF Solver.

Markus N. Rabe and Leander Tentrup.
FMCAD 2015.

[T17]

On Expansion and Resolution in CEGAR Based QBF Solving.

Leander Tentrup.
CAV 2017.

Availability

The latest version of CAQE is available on GitHub.

Legacy Versions

CAQE qbfeval 2017 (2017-07-19) binary release without certification
CAQE version 2 (2016-05-19)

Contact

Markus N. Rabe, Leander Tentrup