5. Post-process a CNF formula¶
After you produce a cnfgen.CNF
, maybe using one of the
generators included, it is still possible to
modify it. One simple ways is to add new clauses but there are ways
to make the formula harder with some structured transformations.
Usually this technique is employed to produce interesting formulas for
proof complexity applications or to benchmark SAT solvers.
5.1. Example: OR
substitution¶
As an example of formula post-processing, we transform a formula by substituting every variable with the logical disjunction of, says, 3 fresh variables. Consider the following CNF as starting point.
After the substitution the new formula is still expressed as a CNF and it is
There are many other transformation methods than OR
substitution.
Each method comes with a rank parameter that controls the hardness
after the substitution. In the previous example the parameter would be
the number of variables used in the disjunction to substitute the
original variables.
5.2. Using CNF transformations¶
We implement the following transformation methods. The none
method
just leaves the formula alone. It is a null transformation in the
sense that, contrary to the other methods, this one returns exactly
the same cnfgen.CNF
object that it gets in input.
All the other methods would produce a new CNF object with the new
formula. The old one is left untouched.
Some method implemented as still missing from the list
Name | Description | Default rank | See documentation |
none |
leaves the formula alone | ignored | |
eq |
all variables equal | 3 | cnfgen.AllEqualSubstitution |
ite |
if x then y else z | ignored | cnfgen.IfThenElseSubstitution |
lift |
lifting | 3 | cnfgen.FormulaLifting |
maj |
Loose majority | 3 | cnfgen.MajoritySubstitution |
neq |
not all vars equal | 3 | cnfgen.NotAllEqualSubstitution |
one |
Exactly one | 3 | cnfgen.ExactlyOneSubstitution |
or |
OR substitution | 2 | cnfgen.OrSubstitution |
xor |
XOR substitution | 2 | cnfgen.XorSubstitution |
Any cnfgen.CNF
can be post-processed using the
function cnfgen.TransformFormula()
. For example to
substitute each variable with a 2-XOR we can do
>>> from cnfgen import CNF, XorSubstitution
>>> F = CNF([ [1,2,-3], [-2,4] ])
>>> G = XorSubstitution(F,2)
Here is the original formula.
>>> print( F.to_dimacs() )
p cnf 4 2
1 2 -3 0
-2 4 0
<BLANKLINE>
Here it is after the transformation.
>>> print( G.to_dimacs() )
p cnf 8 12
1 2 3 4 5 -6 0
1 2 3 4 -5 6 0
1 2 -3 -4 5 -6 0
1 2 -3 -4 -5 6 0
-1 -2 3 4 5 -6 0
-1 -2 3 4 -5 6 0
-1 -2 -3 -4 5 -6 0
-1 -2 -3 -4 -5 6 0
3 -4 7 8 0
3 -4 -7 -8 0
-3 4 7 8 0
-3 4 -7 -8 0
<BLANKLINE>
It is possible to omit the rank parameter. In such case the default value is used.