[  download | overview | publications | license ]

Download

Please see the README file for installation instructions and release notes.

• Source code: QRPcert 1.0.1.

Overview

QRPcert is a tool for extracting Skolem/Herbrand function-based QBF certificates from Q-resolution proofs in QRP format. Skolem/Herbrand functions are represented as AIGs in AIGER format (ascii and binary version supported).

QRPcert is part of QBFcert, a framework for extracting and validating QBF certificates.

For bug reports etc., please contact Mathias Preiner.

Publications

• Paper and talk at SAT 2012 conference.
• A more detailed description of QRPcert can be found here.

License

QRPcert is developed and maintained by Mathias Preiner.
It is released under GNU GPLv3 (see file COPYING, which is part of the distribution).