TNF / INF
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
- 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
- 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
- The formulas used in the experiments
were obtained from the QBF