QRAT Proofs for Bloqqer

Overview

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

Disclaimer

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

Downloads

• Checker for SAT instances
• Checker for UNSAT instances
• Bloqqer with QRAT proving (2014-02-16)*
• Pretty printer for formulas in QDIMACS format
• Script which removes comments from proofs for unsat files
• Script which removes comments from proofs for sat files
• Script for satisfiable formulas
• Script for unsatisfiable formulas
• Log files of the updated version
• Checking statistics: sat-eval10, sat-eval12, unsat-eval10, unsat-eval12

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

Remarks

• 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.

Archive

• Log files of the paper
• Log files of 14.02.14