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’07). Springer LNCS 4501, 244–257, 2007.

Usage

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.