PV4 ⊧ QuAbS: Quantified Abstraction Solverproduces a satisfiability result for a quantified boolean formula

Solver for quantified Booelan formulas (QBF) based on a CEGAR-based abstraction algorithm

Application domain/field

• Quantified Boolean formula (QBF)
• Counterexample guided abstraction refinement (CEGAR)
• QBF satisfiability
• Satisfiability solving

Type of tool

Satisfiability solver

Expected input

Quantified boolean formula

Format:

QCIR (quantified circuit) format.

Expected output

r SAT or r UNSAT

Comments

There is also a prototype that has been parallelized, which is referred to as PQUABS in the SAT '16 paper. They provide a conversion from QCIR to QAIGER