PV4 ⊧ CAQE: Clausal Abstraction for Quantifier Eliminationproduces a satisfiability result for a quantified boolean formula

Solver for quantified boolean formulas (QBF)

Application domain/field

• Quantified boolean formulas (QBFs)
• Boolean theories
• QBF solver

Type of tool

QBF (quantified boolean formulas) solver

Expected input

quantified Boolean formula (QBF) in prenex conjunctive normal (prenex CNF) form

Format:

QDIMACS file format

Expected output

Result code 10 for satisfiable and 20 for unsatisfiable instances. It can also output in the QDIMACS format which has partial assignments to variables.

Internals

Uses PicoSAT, MiniSat, CryptoMiniSat and Lingeling as underlying SAT solver.