QBV, the Quantified Boolean Valdidator, is a tool that validates certificates (proofs) of QBF Solvers. For reference we have implemented the following suite of QBF Validation tools:
squolem, a Skolemization-based QBF solver that generates certificates.
QBV, a certificate validator.
QBFi, a QBF problem inverter.
All of them are available for Download.
The certificate format the we defined makes use of
Skolem-functions for certificates of validity and Q-Resolution
for certificates of invalidity.
For questions about
For a performance comparison, see Statistics.
You should also read the