cnfgen.transformations.substitutions module

AllEqualSubstitution(F, k, invert=False)

Apply all-equals substitution of rank k

F : cnfgen.CNF
formula
k : int
arity of the all-equals substitution
invert : bool
apply the not-all-equal substitution
AndSubstitution(F, k)

Apply AND substitution of rank k

F : cnfgen.CNF
formula
k : int
arity of the or substitution
AnythingButKSubstitution(F, N, k)

Substitution: anything bit C true variables out of N copies

AtLeastKSubstitution(F, N, k)

Substitution: at least k true variables out of N copies

AtMostKSubstitution(F, N, k)

Substitution: at most k true variables out of N copies

ExactlyKSubstitution(F, N, k)

Substitution: exactly k true variables out of N copies

ExactlyOneSubstitution(F, k)

Apply exactly-oine substitution of rank k

F : cnfgen.CNF
formula
k : int
arity of the xor substitution
FlipPolarity(F)

Flip the polarity of variables

F : cnfgen.CNF
formula
FormulaLifting(F, k)

Formula lifting: Y variable select X values

F : cnfgen.CNF
a formula
k : int
arity of the lifting
IfThenElseSubstitution(F)

Apply if-then-else substitution

Each original variable is substituted with a function on three new variables x,y,z which is

if x then y else z

F : cnfgen.CNF
formula
LinearSubstitution(F, k, op, C)

Linear substitution of rank k

Substitute each variable x(i) with a linear form

x(i,1) + x(i,2) + … x(i,k) op constant

F : cnfgen.CNF
formula
k : int
arity of the linear substitution
op : str
an operator among
C : int
constant
MajoritySubstitution(F, k)

Apply Majority substitution of rank k

F : cnfgen.CNF
formula
k : int
arity of the majority substitution
NotAllEqualSubstitution(F, k)

Apply not-all-equals substitution of rank k

F : cnfgen.CNF
formula
k : int
arity of the not-all-equals substitution
OrSubstitution(F, k)

Apply Or substitution of rank k

F : cnfgen.CNF
formula
k : int
arity of the or substitution
VariableCompression(F, B, function)

Vabiable compression transformation

The original variable are substituted with the XOR (or MAJ) of a subset of a new set of variables. The mapping between the original variables and the new ones is given by a bipartite graph

Parameters:
F : CNF

the original cnf formula

B : cnfgen.graphs.BipartiteGraph

a bipartite graph. The left side must have the number of vertices equal to the number of original variables

func: string

Select which faction is used for the compression. It must be one among ‘xor’ or ‘maj’
XorSubstitution(F, k)

Apply Xor substitution of rank k

F : cnfgen.CNF
formula
k : int
arity of the xor substitution
add_description(F, text)

Add the description of a transformation

Parameters:
F : cnfgen.CNF

formula that gets the new description

text : str

text of the description
apply_substitution(formula, subst)

Apply the substitution f to a formula

Applies a substitution to a formula and produces a sequence of clauses.

Parameters:
formula : cnfgen.CNF

formula that gets the new description

subst : function

a function that maps literals to sequences of clauses