View on GitHub

CNFgen

Combinatorial benchmarks for SAT solvers

Download this project as a .zip file Download this project as a tar.gz file

Often we want to increase the hardness of formulas in a controlled way to study their proof complexity or how SAT solvers perform on them.

Usage

CNFgen include two tools with formula transformation capability: cnfgen can apply the transformation after it generates the CNF, and directly outputs the DIMACS of the final formula,

cnfgen --Transform <type> --Tarity <N> <formula_type> <formula_param>

while cnftransform applies transformations to any DIMACS formula in input, using the command line

cnftransform --Transform <type> --Tarity <N> [-i <inputfile>] [-o <outputfile>]

For example, if we want to substitute each variables of a CNF in DIMACS format, given in standard input, with a XOR of 3 new variables and output the formula on standard output it is sufficient to type

cnftransform --Transform xor --Tarity 2

For a list of all implemented transformations you can type either

cnfgen --help-transform

or

cnftransform --help-transform

Available transformations

The cnfgen and cnftransform tools expose the formula transformations implemented in the cnfformula library. Both tools only apply at most one transformation at a time. Via python code there is definitely more flexibility.

Exactly one

We substitute each variable x with a function f(x₁,x₂,…,) over <N> new variables, where the function is true if and only if exactly one of the new variable is true.

cnfgen -T one -Ta <N> <formula_type> <formula_param>
Exclusive OR

We substitute each variable x with the XOR of <N> new variables (x₁,x₂,…).

cnfgen -T xor -Ta <N> <formula_type> <formula_param>
If Then Else

We substitute each variable x with the function over three variables y₀,y₁,y₂ such that if y₀ is true then the value of the function is equal to y₁, otherwise it is equal to y₂.

cnfgen -T ite <formula_type> <formula_param>
All equals

We substitute each variable x with a function f(x₁,x₂,…,) over <N> new variables, where the function is true if and only if the variables are either all true or all false.

cnfgen -T eq -Ta <N> <formula_type> <formula_param>
Not all equals

We substitute each variable x with a function f(x₁,x₂,…,) over <N> new variables, where the function is true if and only if at least two of the arguments are different.

cnfgen -T neq -Ta <N> <formula_type> <formula_param>
Or

We substitute each variable x with the disjunction of <N> new variables (x₁,x₂,…).

cnfgen -T or -Ta <N> <formula_type> <formula_param>
Loose Majority

We substitute each variable x with a function f(x₁,x₂,…,) over <N> new variables, where the function is true if and only if at least half of the variables are true.

cnfgen -T maj -Ta <N> <formula_type> <formula_param>
One dimensional lifting

For each variable x we introduce <N> value variables (x₁,x₂,…) and <N> selector variables (y₁,y₂,…). The value of the original variable is substituted with the value of the xᵢ variables for which the selector yᵢ is active. We want at least one selector to be active.

Concretely the variable x is substituted by ∧ᵢ(yᵢ → xᵢ). Furthermore the clause y₁ ∨ y₂ ∨ … is added to the formula to guarantee that at least one selector is active.

cnfgen -T lift -Ta <N> <formula_type> <formula_param>

Background

Pick a formula F on variables {xᵢ}. We can take a function g:{0,1}ˡ→{0,1} and substitute each variable with the value of function g on l independent copies of the variables. For example if g is XOR and l=2 then the CNF

x ∧ (y v ¬z)

becomes

x₁⊕x₂ ∧ (y₁⊕y₂ v ¬z₁⊕z₂).

Each of the two original clauses must be represented in CNF form: x₁⊕x₂ becomes (x₁ v x₂)∧( ¬x₁ v ¬x₂); and y₁⊕y₂ v ¬z₁⊕z₂ becomes

( y₁ v y₂ z₁ v ¬z₂)∧ (¬y₁ v ¬y₂ z₁ v ¬z₂)∧ ( y₁ v y₂ ¬z₁ v z₂)∧ (¬y₁ v ¬y₂ ¬z₁ v z₂)

Some of the transformations can be a little bit more complex than that, but the XOR is a good example of how to make a formula harder.