Making IP = PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms – Artifact
Eszter Couillard, Philipp Czerner, Javier Esparza, Rupak Majumdar · Zenodo (CERN European Organization for Nuclear Research) · 2023
This is the artifact for the submission “Making IP = PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms”. Within the paper, we develop a new approach to interactively certify BDD algorithms. We implemented this approach as `blic`, a certifying QBF solver. This tool is evaluated against other QBF solvers. The artifact consists of the source code for `blic`, as well as the data and other tools necessary to replicate the empirical claims of the paper.