Another idea is, if we have a formula which is very small, let's say,
at most three variables,
then we can always find a small CNF which is logically equivalent to it.
Now, the idea is,
we want to transform our big formula Phi to a conjunction of
many small formulas using these extra variables
in such a way that satisfiability is preserved.
If we then transform the small variables to CNF,
then the resulting formula is a CNF itself.
More precisely, for every subformula Psi,
we define its name.
If the subformula is a literal,
so a variable or the negation of a variable,
it's just the literal itself.
But otherwise, it's the name we introduced it for it,
and that's a fresh variable.
Now, the Tseitin transformation is defined to
be the CNF consisting of the following ingredients.
First, we have the clause, the unit clause,
just the name of the whole formula itself.
Next, for every subformula, we do something.
If the subformula is of the shape the negation
of Psi and this negation of Psi has name Q,
then we add Q bi-implication,
not the name of Psi.
That is what we add,
and we make CNF out of this.
For subformulas being a binary operation onto other subformulas,
let's say, Psi 1 and Psi 2,
and the binary operation, let's call, diamond.
So, this can be disjunction or conjunction or implication or bi-implication.
We introduce the following.
We give the name Q to the whole formula Psi 1 diamond Psi 2.
Now, we compute the CNF of Q bi-implication the name of Psi 1 diamond the name of Psi 2.
Let's give an example.
Here, we have an arbitrary formula in which many binary operations occur,
and we have a number of non-variable subformulas B,
C, and D, and also, the formula itself.
Now, that Tseitin transformation consists of the name of the whole formula N Phi
and the CNF of N Phi bi-implication B bi-implication C,
since the whole formula is the bi-implication of the formula
named B and the formula named C. Next,
B is the conjunction of not S and P. So,
we compute the CNF of B bi-implication not S and P, and so on.
In this way, we get the whole Tseitin transformation.
Now, we consider preservation of satisfiability of the Tseitin transformation.
We will show that if Phi is satisfiable,
then the Tseitin transformation is disatisfiable,
and also the other way around.
But first, assume Phi is satisfiable.
That means, it admits a satisfying assignment.
Now, the idea is, we extend this to the fresh variables.
If we have a subformula Psi,
then we give N Psi the value of the subformula.
Then, this yields a satisfying assignment for the Tseitin transformation.
First, we had a satisfying assignment of the whole formula,
so the whole formula yields true.
So, N Phi yields true, too.
If we have a subformula not Psi,
then we observe that Q bi-implication not N Psi yields true,
if Q is the name of not Psi.
That is how we defined the values of the names.
So, this Q bi-implication not N Psi yields true.
So, also, it's a CNF yields true.
If we have a subformula Psi 1 diamond Psi 2
for a binary operator diamond and it has the name Q,
then Q bi-implication N Psi 1 diamond N Psi 2 also yields true by definition.
By this assignment, the definition how we gave values to our ends.
So, this yields true,
so also, its CNF yields true.
So, we conclude that from
the satisfying assignment of Phi which we extend to the fresh variables,
we get a satisfying assignment of T Phi.
So, satisfiability of Phi implies satisfiability of T Phi.
Conversely, assume that T Phi is satisfiable,
and that is, it admits the satisfying assignment.
Now, we apply the same satisfying assignment to the original formula
Phi in which only the original variables occurs and not the extra variables.
But since Q bi-implication N Psi 1 diamond
N Psi 2 yields true for a subformula Psi 1 diamond Psi 2 having name Q,
we obtain that every subformula Psi of Phi gets the value of N Psi,
and the same for not N Psi.
Since N Phi yields true as part of the Tseitin transformation,
we obtain that the whole formula Phi yields true.
So, Phi is satisfiable.
Combining both directions, we get that Phi is
satisfiable if and only if T Phi is satisfiable.
Now, we still needs to compute the formulas
CNF of the small formulas we saw in this construction.
The small formulas all were of the shape,
the name of the formula bi-implication,
either a negation or a binary operator on two other variables.
That can be done as follows.
If it's a negation, well,
we only need to compute the CNF of P bi-implication not Q,
and that is P or Q and not P or not Q.
The only way P is equivalent to not Q is
that P or Q should be true and P or Q should be false,
which is stated in this formula.
By a truth table,
you can easily check that this is equivalent.
Next, we need to consider the binary operators.
So, let's consider P bi-implication Q and R. Well,
that has this simple CNF and the same for disjunction has a simple CNF,
and for bi-implication we have this one.
We did not give the formula here for implication,
but if we just write Q implies R to be not Q or R,
we can use the formula for or.
