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.