The transformation LiteralSubstitution substitutes literals in a given formula. For example, given the formula
A & ~B | B & ~D, and the substitutions
~B -> C
B -> E
D -> ~A
then the substituted formula is
A & C | E & A.
The difference to the
substitute operation on formulas is, that such a substitution can only be applied from variables to arbitrary formulas, whereas the
LiteralSubstitution operates on literals and therefore can replace positive and negative literals differently.
Note that both substitutions perform a parallel substitution:
That is, the formula
(X | A) & (Y | B) & (Z | C) with the substitutions
A -> B
B -> C
(X | B) & (Y | C) & (Z | C), and not
(X | C) & (Y | C) & (Z | C).
The mapping that should be applied can either be given to the transformation as a parameter by using the parameterised constructor, or, if one wants to add mappings in hindsight, by adding substitutions with
The Anonymizer transforms the given formula into one where all names of the formulas' variables are replaced by new ones. This is usually used when the original variable names contain domain-specific knowledge and one wants to anonymize the formula. One can define how the new variables are named: A prefix with which the variable shall begin and a number where to start. The default values are
0, meaning the anonymized variables will be
v0, v1, v2, ... .
Note that the order of the new variables is based on the alphabetical order of the original variables (not in the order in which the variables occur in the formula). For example, when anonymizing the formula
A & C | B, the transformed formula is
v0 & v2 | v1 (and not
v0 & v1 | v2, as one might expect).
2.3.0 The method
getSubstitution() returns the current substitution map from the anonymizer. This can be helpful if you want e.g. translate an anonymized formula back to its original one.
Using quantifier elimination transformations, one can eliminate quantified variables from a formula. There is the existential quantifier elimination ExistentialQuantifierElimination, which eliminates the existential quantifier
∃ in a given formula, and the universal quantifier elimination UniversalQuantifierElimination, which respectively eliminates the universal quantifier
Both transformations use the Shannon expansion for eliminating the quantifier, see (Boolean quantification in a first-order context by Seidl and Sturm). In short: the formula is expanded once with the variable to eliminate substitued by false, once by true. For an existential quantifier elimination the two formulas are then disjoined, for an universal quantifier elimination they have to be conjoined.
Firstly, consider the
ExistentialQuantifierElimination with the formula
∃C: A & B & (C | D).
The transformation propagates the statement "there exists the variable
C" through the formula, which yields
A & B | A & B & D and can be simplified to
A & B, meaning
A & B is a necessary and sufficient condition in order that there exists an assignment for
C in order to evaluate the whole formula to true.
Secondly, consider the
UniversalQuantifierElimination with the formula
∀C: A & B & (C | D).
f3 = A & B & (C | D). Then the statement is: "
f3 holds for all
C", regardless whether
C is assigned to
false. Simplified by the
UniversalQuantifierElimination, this yields
A & B & D, meaning
A & B & D is a necessary and sufficient condition in order that for all assignments of
C the formula can evaluate to true. The
UniversalQuantifierElimination can also evaluate to
false: For example,
∀C, D: A & B & (C | D), that is "
f3 holds for all
C and all
D", is unsatisfiable.
Both quantifier elimination transformations cannot be cached since they are dependent on the set of literals to eliminate.
Here is a code snippet for this example for the existential quantifier elimination (analogous for the universal quantifier elimination):
Formula Factory Importer
The FormulaFactoryImporter imports a formula from another formula factory into the current formula factory. For example, the following code snippet imports the formula
f1 from the formula factory
f to the new formula factory
result is equivalent to
f1 but belongs to the formula factory