QuAbS

QuAbS (Quantified Abstraction Solver) is a certifying solver for quantified Boolean formulas (QBF) based on a CEGAR-based abstraction algorithm.
It accepts arbitrary Boolean formulas in QCIR format.

QBFEval2018 results: 1st place in prenex non-CNF track.
QBFEval2017 results: 3rd place in prenex non-CNF track.

For solving QBFs in QDIMACS file format, see our CNF solver CAQE.

Paper

[HT18]

Solving QBF by Abstraction

Jesko Hecking-Harbusch, Leander Tentrup
GandALF 2018

[T16]

Non-prenex QBF Solving Using Abstraction

Leander Tentrup
SAT 2016

Availability

Source code is available at GitHub.

Contact

Leander Tentrup