In this lecture we will see how to establish satisfiability of an arbitrary propositional formula which is not a CNF. We saw that for CNFs we had efficient procedures to establish satisfiability, but now if the formula is not a CNF, what to do in that case? Well, then we want to transform the formula to a CNF preserving satisfiability. Then we can use the DPLL based SAT to this CNF and establish satisfiability of the CNF and hence of the original formula. Current SAT solvers do this all automatically, but now we want to see how it works internally. The first simple approach is find a CNF that is logically equivalent to the given formula. Well, two important observations, one is the good news, this is always possible, but the other is the bad news, the resulting CNF is often unacceptably large. The size can be exponential in the size of the original formula. In this lecture we will show how it is possible in every case and we'll also show why it may blow up, so why this approach should be avoided, and then in the next lecture, we will present the alternative approach, the Tseitin transformation which is used in practice. But it's good to understand why the straightforward approach does not work. For any propositional formula, phi, we can make it's truth table, and for any zero faults in this truth table, we can make a corresponding clause. Let's give an example on any formula on three variables p,q, and r. Doesn't matter what the formula is we just look at the truth table. Well, pick a zero in the truth table of phi. For instance, this is zero which is indicated right now. Now, we want to make a clause having a zero on this position and a one everywhere else. How to do this? Well, this zero is obtained for the case where p is false, q is true, and r is false, well, then we can make the clause. P or not q or r having exactly this truth table. It's only false, if p is false, q is true, and r is false, and in all other cases it yields true. The same we can do for the next zero into truth table of phi and also for the last one and in general, for every zero we can make a corresponding clause. Then the observation is if we take the conjunction of these corresponding clauses, we get a CNF having exactly the same truth table as phi by constriction, so it is logically equivalent to phi. So, this shows that it is always possible to find a CNF which is logically equivalent to any arbitrary propositional formula phi. It always works and if the truth table of phi contain k 0's, we obtain a CNF consisting of k clauses. The drawback is this k may be very large. If there are any variables then the truth table has 2 to the power n rows which is exponential in n. All of the clauses found in this constriction have exactly n literals. Sometimes a smaller CNF which is logically equivalent to phi may exist having clauses of less than n literals. For instance, p and not q or r is a CNF with only two clauses, but if you build a truth time table you will see that it has five zeros in the truth table. But for some formulas the exponential number of clauses is unavoidable which we will show now by an example. We take the by implication n variables p1, p2, p3, until pn. This formula yields true if and only if an even number of pi's has the value false. This can be established just by checking. Now, the key argument is the following claim. Let X be a CNF which is logically equivalent to this particular formula phi. Then every clause C in X contains exactly n literals. Well, let's prove it. Assume not, then some pi does not occur in a clause C of X since it is assumed that there is a clause with less than n literals. But if pi does not occur into clause C, then you can give values to the remaining variables such that C yields false. Since X is the conjunction of the clauses also X yields false and this is independent of the value of pi. So, swapping values of pi does not swapp values of X, and that's contradicting two logical equivalence, since phi has the property that if you swapp any value of any variable it always swaps the result. The truth table of this particular formula phi contains two to the power n rows, and exactly half of them yields zero. So, there are exactly two to the power n minus one zeros in the truth table. Every clause of exactly n literals use exactly one zero into truth table. We just saw in the claim that the CNF of these phi only has clauses with exactly n literals. So, every of these clauses yields exactly one zero. So, we need two to the power n minus one of such clauses to get a formula which is logically equivalent to phi, that means it has the same truth table. So, for this phi the exponential size is unavoidable. Summarizing, we saw that for any propositional formula phi it is possible to find a logically equivalent CNF. But the size of the CNF may be exponential, and that not only occurs in the artificial example as we construct it, but it also occurs in practice. So, in order to apply CNF based satisfiability solving on an arbitrary propositional formula, we need something else. That will be the topic of the next lecture that we will present to the Tseitin transformation by introducing extra variables, we can find a formula which does the job for us. Thank you.
