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