CADET - A solver for 2QBF

CADET (CAl DETerminizer) is an algorithm for determining the truth of quantified boolean formulas (QBFs) based on a new solving principle. For a given QBF, the algorithm incrementally constructs the Skolem function, which is a proof of the truth of the formula. Currently the algorithm is limited to a single quantifier alternation (2QBF).

NEW! I released a revised version of CADET on Github!


[RS16] Incremental Determinization.
with Sanjit Seshia.
SAT, 2016.


The original CADET (v1.0) binaries are available below. Please visit the new Github website for newer releases!

CADET OSX binaries

CADET linux binaries


The tool was developed by Markus Rabe. Feel free to contact me.