# Formula Transformations

A formula transformation takes a formula as input and returns another formula. A formula transformation is a special case of a Formula Function but always returns a formula. We distinguish the following kinds of formula transformations:

- Normal Form Transformations, e.g. conjunctive normal form (CNF) or disjunction normal form (DNF)
- Simplifier Transformations, which try to minimize or simplify the formula
- Other Transformations for other useful transformations such as anonymizing a formula

Analogously to the formula functions and the formula predicates, formula transformations can be executed on formulas with the `.transform()`

method. In the following example the `DistributiveSimplifier`

is executed on the formula `f1`

with activated caching:

Caching can also be deactivated by calling the overloaded method with flag `false`

:

The last parameter of the `.transfom()`

method indicates whether the result of the transformation should be cached in the formula. If you have an expensive computation which is likely to be executed more than once on formulas, it is a good idea to cache the result.

The result of any transformation in this chapter is another formula. Depending on the transformation the resulting formula will be *equisatisfiable*, *equivalent* or neither of both compared to the input formula.

Equivalence vs Equisatisfiability

Two formulas `f1`

and `f2`

are (logically) *equivalent* if both formulas evaluate to the same truth value *for all* assignments. With `eval(f1, a)`

we denote the truth value of the formula `f1`

when evaluated under assignment `a`

. Formulas `f1`

and `f2`

are equivalent, if for *every* assignment `a`

holds:

In contrast, two formulas `f1`

and `f2`

are *equisatisfiable* if either both are *satisfiable* or both are *unsatisfiable*, i.e. if the following holds:

Note that *equisatisfiability* is implied by *equivalence* but not the other way round.

Consider the example:

The formulas are both satisfiable, i.e. they are equisatisfiable. But they are not equivalent. For example, the assignment `a = {~A, B, ~C}`

yields `eval(f1, a) = true`

, but `eval(f2, a) = false`

.

For more information check out Equisatisfiability in Wikipedia.