Validating QBF Decisions
About -- Download -- Statistics

About QBV

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 a performance comparison, see Statistics.

For questions about QBV or squolem, contact Christoph M. Wintersteiger.

You should also read the license.

 

 

QBV News

2010-10-26: Version 2.0 released
2007-01-28: Version 1.03 released

Squolem News

2010-10-30: Version 2.01 released
2010-10-26: Version 2.00 released
2007-01-28: Version 1.03 released

 

 

Support

This research is currently supported by an award from IBM research and a grant from the Swiss National Science Foundation.