PV4 Uniquegenerates interpolant graphs from CNF formulae

Application domain/field

Expected input

Expected output

Internals

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

Links

https://github.com/fslivovsky/unique

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.