This lecture is about the Tseitin transformation. The Tseitin transformation is a linear transformation from an arbitrary propositional formula to CNF, preserving satisfiability. It goes back to a paper by Tseitin from 1966. This Tseitin transformation is used in all current SAT solvers. The key idea is that we do not try to find a formula which is logically equivalent to Phi, but we add extra variables. More precisely, we give a name to every subformula, except for literals, and we use these extra names as fresh variables in our formula. So, the resulting formula is not only on the original variables, but also on these fresh variables. 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. The small formulas for CNF are easy to compute. For instance, if we consider the one with disjunction P bi-implication Q or R, we want to transform this to CNF. How to do that? Well, first we observe that the bi-implication is just a conjunction of two implications, one from left to right and one from right to left. If we consider the implication from left to right, we see P implies Q or R is equivalent to not P or Q or R, which is a clause itself. The other direction Q or R implies P is equivalent to not Q or R or P, and by De Morgan rules, it can be written in this way. By applying distributivity, we get these two clauses. So, we conclude that the CNF of this small formula consist of these three clauses, and in this way, we can do all these computations. Concluding, for every propositional formula Phi, it's Tseitin transformation T Phi is easily computed. The size is linear in the size of Phi, so there is no exponential blow up, not even a polynomial blow up, only linear, and it preserves satisfiability. A formula Phi is satisfiable if and only if T Phi is satisfiable. Even more, it not only gives CNF, it gives a 3-CNF. All clauses occurring in T Phi have at most three literals. This Tseitin transformation is used in all current SAT solvers.
