CAQE (Clausal Abstraction for Quantifier Elimination) is a certifying solver for quantified Boolean formulas (QBF) based on the CEGAR-based clausal abstraction algorithm.
- 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.
Unix like operating system and a modern C compiler, tested on Linux/gcc and macOS/clang.
Installation & Usage
Linux/macOS Compile from source:
$ ./configure && make
macOS Install CAQE using Homebrew:
- Tap reactive systems repository:
$ brew tap reactive-systems/react
- Install CAQE from source:
$ brew install caqe
$ ./caqe <instance.qdimacs>
Certificates are given as valid AIGER files with some additional conventions:
- The symboltable defines the original variable names from the QDIMACS file
- There is one additional output which must be the last output and it indicates whether the certificate is a Skolem or Herbrand certificate (value 1 and 0, respectively).
QDIMACS file encoding an equality constraint:
c equality.qdimacs p cnf 2 2 a 1 0 e 2 0 -1 2 0 1 -2 0
The corresponding Skolem certificate is
aag 1 1 0 2 0 2 2 1 i0 1 o0 2 o1 result c equality.cert.aag
$ make certification)
$ ./certcheck <instance.qdimacs> <certificate>
- Output of
certcheckis an AIGER file that contains exactly one (bad) output.
- The output can be verified by a SAT solver: converting using
aigtocnffrom AIGER toolset and solving the resulting DIMACS file using a standard SAT solver.
- An UNSAT result witnesses the correctness of the certificate (there is no input such that the bad output is enabled).
$ ./certcheck equality.qdimacs equality.cert.aag | aigtocnf | picosat returns unsatisfiable, hence, the certificate is correct
Copyright © 2015-2016 Saarland University