CADET is a solver for quantified Boolean formulas with a forall-exists quantifier alternation (2QBF). The solver is based on the Incremental Determinization algorithm published in SAT 2016 was written by Markus N. Rabe. As of 2018, CADET is one of the fastest and most reliable solvers for 2QBF formulas. It won second price in the 2QBF track of QBFEval and can also prove its results little overhead, which is unique in the current landscape of QBF solvers.
Here we discuss how to encode the formula ∀ x1 x2: ∃ y: y = (x1 & x2) and how to interpret CADET’s results.
c This QDIMACS file encodes the formula c forall x1, x2 exists y. y <-> x1 & x2. c x1 is represented by number 1 c x2 is represented by number 2 c y is represented by number 3 p cnf 3 3 a 1 2 0 e 3 0 1 -3 0 2 -3 0 -1 -2 3 0
Lines starting with
c are comments. The header is the line starting with
p cnf followed by two numbers indicating the number of variables and the number of clauses. The lines starting with
e are quantifiers introducing universally quantified variables 1 and 2, and the existentially quantified variable 3. The remaining three lines each state one constraint (a clause). The last line, for example states that 1 must be false or 2 must be false or 3 must be true. It is easy to check that the three constraints (clauses) together require y to be the conjunction of x1 and x2: Simply interpret the clauses as implications -x1 -> -y, -x2 -> -y, and (x1 & x2) -> y.
CADET will solve this file easily:
$ ./cadet formula.qdimacs
Processing file "formula.qdimacs". CADET v2.3 SAT
This indicates that the formula is satsifiable (i.e. true, as we consider only closed formulas).
To prove formulas true CADET constructs a function assigning a value to y for every assignment to x1 and x2 (a Skolem function). For many applications, such as circuit repair, safety games, and strategy extraction for LTL synthesis we are interested in the function that CADET computed as it represents the solution of the encoded problem. With the command line argument
-c <filename> CADET outputs this function as an AIGER circuit:
$ ./cadet -c result.aig formula.qdimacs
The result is written to the file
result.aig, which is typically a bit bloated and it is intended to be minimized after generation. For example, you can use the following command to minimize circuits with ABC:
$ abc -c "read result.aig; dc2; write result.aig"
After the minimization a circuit with a single AND-gate remains:
aag 3 2 0 1 1 2 4 6 6 4 2 i0 1 i1 2 o0 3
To view a human-readable version of the circuit as shown above you have to convert the AIGER binrary formag
.aig to the AIGER ASCII format
.aag using the tool
aigtoaig available in the AIGER toolset.
CADET can be built from source with both clang and gcc. You can find pre-built binaries of CADET for Linux and OSX. The testing scripts require Python 2.7.
To compile the solver type:
$ ./configure && make
To make sure the solver works correctly execute the test suite:
$ make test
One of the test cases will timeout as part of the testsuite and a number of tests will return with the result UNKNOWN, which is intended.
The most common use case for the solver is to solve formulas specified as a QDIMACS file.
$ ./cadet file.qdimacs
You can also pipe QDIMACS into the solver:
$ cat file.qdimacs | ./cadet
CADET reads files in both QDIMACS and AIGER format. Files can be zipped with gzip, but must then end with the file extension gz or gzip. Details on the interpretation of AIGER files as 2QBF can be found in the user guide. Note that the current AIGER input is being phased out in favor of the QAIGER format, a new standard being developed in the QBF community.
CADET is able to prove (or certify) its results. As 2QBF formulas in QDIMACS have a forall-exists quantifier alternation, proofs for UNSAT results are given as an assignment to the universally quantified variables. Proofs for SAT results are given as a circuit, mapping assignments to the universally quantified variables to assignments to the existentially quantified variables.
Certificates for UNSAT results are written to stdout according to the QDIMACS standard. To print output according to the QDIMACS standard, use the
--qdimacs_out flag. CADET checks UNSAT certificates internally by default.
With the command line option
-c [file] CADET writes the SAT certificate for true 2QBF. You can either specify a file name to which the certificate should be written (ending in
.aig) or you can specify
sdtout to let CADET print the certificate on the terminal. For example, type:
$ ./cadet -c certificate.aag file.qdimacs
As soon as you work with certificates you may want to install the AIGER tool set and the ABC. The distribution of CADET comes with several scripts that demonstrate how to generate, simplify, and check certificates using ABC and the AIGER tool set.
UNSAT results are checked internally by default. You can double check them by asserting the assignment to the universals in the CNF of the QDIMACS and querying a SAT solver.
For checking SAT certificates you have two options: By default CADET produces certificates that can be checked by Certcheck, which was written by Leander Tentrup. Certcheck comes with the distribution of CAQE. To produce certificates that are compatible with QBFcert add
--qbfcert option to the command line.
Note that QBFcert standard is only compatible with the ASCII format of the AIGER standard, so be sure that the certificate file name ends with
.aag. Also, be aware that QBFcert certificates cannot be minimized by ABC.
Incremental Determinization. Rabe and Seshia. SAT, 2016.
Encodings of Bounded Synthesis Faymonville, Finkbeiner, Rabe, Tentrup. TACAS, 2017.
I am indebted to my collaborators, colleagues, and friends who inspired and supported me during this project. In particular, I want to mention Leander Tentrup who contributed some code to this project. I also want to thank Armin Biere and Will Klieber for fruitful discussions about various aspects of SAT and QBF solving. I also want to thank Armando Solar-Lezama, Baruch Sterin, S. Akshay, Supratik Chakraborty, and many others who contributed benchmarks and insights into their tools.