[  download | overview | publications | license ]

Download

QRPcheck requires PicoSAT (see the README file for installation instructions and release notes).

• Source code: QRPcheck 1.0.3.

Overview

QRPcheck is a tool for extracting and checking clause (cube) resolution proofs of unsatisfiability (satisfiability) in binary or ascii QRP format. Further, given a proof of satisfiability, QRPcheck supports optional checking of the validity of the set of input cubes given.

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

For bug reports etc., please contact Aina Niemetz.

Publications

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

License

QRPcheck is developed and maintained by Aina Niemetz.
It is released under the GNU GPLv3 License (see file COPYING, which is part of the distribution).