Description

The ProverBox includes a preprocessor for quantified Boolean formulas which transforms them such that they are often significantly easier to solve.

It reads QBF formulas in conjunctive normal form in QDIMACS format and attempts to reduce the number of universal variables by selectively applying universal expansion and resolution of existential variables. In addition, it is capable of various standard simplification techniques. The output is again in QDIMACS format.

For a more detailed description of the process, please refer to the corresponding paper:

U. Bubeck and H. Kleine Büning.
Bounded Universal Expansion for Preprocessing QBF.
Proc. 10th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2007), Springer LNCS 4501, pp. 244–257, 2007.
[PDF Accepted Author Manuscript] [Original Publication at www.springerlink.com]

Usage

• With the GUI:
  First, switch to QBF* as specification language (use the menu item Language | Select or type lang "qbf*" on the command prompt). This setting will be remembered next time you start the ProverBox.
  To invoke the preprocessor, type qdimacspreprocess on the command prompt. A file selector box will ask you to locate the input file. The result will be written into a new QDIMACS file in the same location with "-out" appended to the original filename.
  
  
• Without the GUI:
  You can preprocess a file /tmp/file.qdimacs by typing the following in the system shell:
  java -Djava.awt.headless=true -jar proverbox.jar 'lang "qbf*"' 'qdimacspreprocess "/tmp/file.qdimacs"' exit