PV4 ⊧ CADET: Cal Incremental Determinizerproduces a satisfiability result for a 2QBF

Application domain/field

• QBF solving
• 2QBF solving

Type of tool

2QBF solver

Expected input

2QBF formula

Format:

QDIMACS or QAIGER format

Expected output

• SAT if 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).
• UNSAT if the formula is unsatisfiable. The tool will then give an assignment for all universally quantified variables. Results are written in QDIMACS format to stdout.

Internals

Uses PicoSAT

Comments

CADET is a 2QBF (Quantified Boolean formulas with forall-exists quantifier alternation) solver