CAQE

CAQE (Clausal Abstraction for Quantifier Elimination) is a certifying solver for quantified Boolean formulas (QBF) based on the CEGAR-based clausal abstraction algorithm.

Paper

CAQE: A Certifying QBF Solver.

Markus N. Rabe and Leander Tentrup.
FMCAD 2015.

On Expansion and Resolution in CEGAR Based QBF Solving.

Leander Tentrup.
CAV 2017.

Download

Prerequisites

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:

  1. Tap reactive systems repository: $ brew tap reactive-systems/react
  2. Install CAQE from source: $ brew install caqe

Usage $ ./caqe <instance.qdimacs>

Certification

Format

Certificates are given as valid AIGER files with some additional conventions:

Example

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

Checking Certificates

Example

$ ./certcheck equality.qdimacs equality.cert.aag | aigtocnf | picosat returns unsatisfiable, hence, the certificate is correct

Contact

Markus N. Rabe, Leander Tentrup

Copyright © 2015-2016 Saarland University