PV4 ⊧ CADET: Cal Incremental Determinizerproduces a satisfiability result for a 2QBF
- QBF solving
- 2QBF solving
Type of tool2QBF solver
Expected input2QBF formula
Format:QDIMACS or QAIGER format
SATif the formula is satisfiable. You can also ask for the solution (assignments for all quantifiers) that CADET has computed (will be given as an AIGER circuit).
UNSATif the formula is unsatisfiable. The tool will then give an assignment for all universally quantified variables. Results are written in QDIMACS format to stdout.