• 27-11-2015: New bloqqer release (version 37) with BLE and minor bug fixes
  • New bloqqer release (version 35) with QRAT proofs and API


Bloqqer is a preprocessor for quantified Boolean formulas. It implements the following preprocessing techniques:

  • Quantified Literal Elimination
  • Quantified Blocked Clause Elimination
  • Quantified Covered Blocked Clause Elimination
  • Quantified Covered Tautology Elimination
  • Quantified Hidden Tautology Detection
  • Quantified Hidden Blocked Clause Elimination
  • Subsumption
  • Variable Expansion
  • Equivalence Detection


[ bloqqer-037-8660cb9-151127.tar.gz ]
[ bloqqer-035-f899eab-141029.tar.gz ]
[ bloqqer-031-7a176af-110509.tar.gz ](version of CADE'11)

For additional information please refer to the included README file or run the --help option.

Talk Slides

Slides of our related talk presented at CADE'11 may be found here.

Experimental Results

Find more details on the experiments presented in our CADE'11 paper as well as the logfiles.