[ overview | workflow | format | certified | download | license ]
QBFcert is a framework for resolution-based extraction and validation of certificates for Quantified Boolean Formulas (QBF). QBFcert supports QRP format for resolution-based traces and proofs. The corresponding QBF certificate is represented in AIGER format.
QBFcert is QBF- and SAT-solver independent, i.e., it is possible to plug any QBF resp. SAT solver into the framework as long as the QBF solver is able to produce resolution-based traces or proofs in binary or ascii QRP format.
Input/Output FormatQBFcert supports ascii and binary QRP format for resolution-based traces and proofs. The corresponding QBF certificate is represented as a set of And-Inverter-Graphs (AIGs) in either ascii or binary AIGER format.
Note that CertCheck generates a propositional formula in DIMACS format.
Certified InstancesHere is a list of instances that were certified with QBFcert (with QRPcheck v1.0.3, QRPcert v1.0.1, CertCheck v1.0.1) within a time limit of 1800 seconds and a memory limit of 7 GB:
See the README file for instructions and release notes, which is also part of the distribution.
Source Code (individual tools)
QBFcert is maintained by Aina Niemetz and Mathias Preiner.