QRAT Proofs for Bloqqer


Bloqqer is a preprocessor for quantified Boolean formulas. The public version is available at the bloqqer website.


The content of this page is for reviewing only. In the case of acceptance we will publish the code of our tools.


* compared to the version used for the experiments in the paper, this version contains some fixes and is able to solve 9 additional formulas.


  • The tools provided above are internal development versions. Please refer to the scripts run_sat.sh and run-unsat.sh for an explanation how to run them (solving + verifying the proof). Usability will be improved for the public release.
  • For producing QRAT proofs with bloqqer use the option --qrat=file
  • The proofs of formulas Adder2-4-s-shuffled and adder-4-sat-shuffled cannot be verified with the standard options of Bloqqer, because miniscoping is used. However, our checkers do not implement miniscoping (i.e., the quantifier order of the prefix is used). This is only an implementation issue and an extension will be provided in the future. If miniscoping is disabled and the excess limit (bounds for variable elimination) is increased, then bloqqer can solve this formulas as well and the proof can be verified.
  • The formulas used in the experiments were obtained from the QBF Gallery.