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


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.



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).