PV4 Uniquegenerates interpolant graphs from CNF formulae

Application domain/field

Expected input

Expected output


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



Related papers

Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing (CAV '20)

Last publication date

14 July 2020

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.