PV4 ⊧ Uniquegenerates interpolant graphs from CNF formulae

Application domain/field

• Gate extraction
• Quantified Boolean Formulas (QBFs)

Expected input

• PCNF formula (QDIMACS)
• prenex non-CNF QBF (QCIR)
• DQBF with CNF matrices (DQDIMACS)

Expected output

• interpolants represented as AIG (And-Inverter Graphs)

Internals

• Gate detection
• Gate extraction

Uses ItpMiniSat, a modified version of MiniSat, bundled with the ExtAvy model checker