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


Given a QBF input formula F and its certificate CF generated by QRPcert, CertCheck transforms F into an AIG and merges it with CF. The resulting AIG is then translated into a propositional formula in CNF, which can be used to validate the correctness of certificate CF. If the generated CNF is unsatisfiable, CF is valid and hence represents a valid (counter-)model of F. If the CNF is satisfiable, CF is invalid.

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

For bug reports etc., please contact Mathias Preiner.



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