[q]bfGen - A Generator for SAT and QSAT Formulas

Overview

The basic workflow of this tool is summarized in the following pichture:

Disclaimer

• This version of [q]bfGen is published for reviewing purposes only.
• No further usage rights than for reviewing are granted and further distribution is not allowed.
• No warranty is given.

Downloads

Please note that this version of [q]bfGen is a first prototype released to demonstrate the features described in the paper.

Download the prototype as executable jar or the sources.

Run [q]bfGen with:

java -jar qbfGen.jar random.xml fileName numberOfFormula [-p]

• random.xml: The random model specified according to the XML Schema formula.xsd.
• fileName: The prefix, the file names of the generated formulas should start with.
• numberOfFiles: The number of formulas which is generated for each setting (within the XML files also parameters may be specified).
• -p: quantifiers are omitted, i.e., propositional formulas are printed

Example for a random model specification for the Shapes described in the paper.

Detailed documentation will follow in the public release.

Experiments

[q]bfGen makes a wealth of experiments and studies without any programming effort possible. A first example of potential research directions is given in the following. To test [q]bfGen we generated formulas based on the extended fixed shape model for QBF. The generated formulas have a quantifier prefix of the form forall X exists Y, where the size of X is m and the size of Y is n. The matrix is a conjunctions of S-constraints. An S-constraint is a balanced tree of alternating disjunctions and conjunctions. In the following, we assume that the matrix of the formula is structured as follows:

The number of S-constraints is given by L = c*n, where c is a constant and n is the number of an existential variable. First experminental results when solving such formulas are shown in the following:

• Download the random model in XML.
• Download the formulas (about 45 MB).

The curves are obtained by running the state-of-the-art QBF solver DepQBF on 200 formulas on each data point, i.e., we ranged the constant c from 2 to 4 with a step width of 0.2.5. The left image shows the number of solved formulas for n=10,20,30,40,50,60. We clearly see that the probability that a formula is satisfiable changes from left to right. The changes take place at about c=3.2. At this time, we also observe a peak in the average runtime (cf. right image).

Here we observe a similar behavior as in plain SAT formulas. This random model offers a multitude of interessting settings for further expermiments with the various parameter settings, issuing interessting questions for further study. Also the formulas are well suited for the evaluation of solvers as (i) their truth value is predictable and (ii) their "difficulty" is customizable.

Further Random Models

• 2+p sat by R. Monasson, R. Zecchina, S. Kirkpatrick, B. Selman, and L. Troyansky
  • random model for formulas of propositional logic in CNF with clauses of size 2 and 3
  • Parameters:
    • N: number of variables
    • M: number of clauses
    • M*p: number of clauses with 3 literals
    • M*(1-p): number of clauses with 2 literals
  • Download random model description for M=5, N=20,21,22,23,24,35, p=0.5
• Simple non-PCNF QBF model
  • Simple example where quantifiers occur inside the formula
  • Download random model description

Known Issues

• parameter values are only integers (workaround: use calc for describing a float)
• calc supports only very basic arithmetics +, -, *, / where the Arguments are numbers or $ for the parameter value (workaround: use multiple parameters)
• for calc one space has to be added between operator and operands