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!
The tool was developed by Markus Rabe. Feel free to contact me.