Editing Conjunctive normal form (section)

===Other approaches===
Since all propositional formulas can be converted into an equivalent formula in conjunctive normal form, proofs are often based on the assumption that all formulae are CNF. However, in some cases this conversion to CNF can lead to an exponential explosion of the formula. For example, translating the non-CNF formula

<math display="block">(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \ldots \vee (X_n \wedge Y_n)</math> 

into CNF produces a formula with <math>2^n</math> clauses:

<math display="block">(X_1 \vee X_2 \vee \ldots \vee X_n) \wedge (Y_1 \vee X_2 \vee \ldots \vee X_n) \wedge (X_1 \vee Y_2 \vee \ldots \vee X_n) \wedge (Y_1 \vee Y_2 \vee \ldots \vee X_n) \wedge \ldots \wedge (Y_1 \vee Y_2 \vee \ldots \vee Y_n).</math>

Each clause contains either <math>X_i</math> or <math>Y_i</math> for each <math>i</math>.

There exist transformations into CNF that avoid an exponential increase in size by preserving [[Boolean satisfiability problem|satisfiability]] rather than [[logical equivalence|equivalence]].{{sfn|Tseitin |1968}}{{sfn|Jackson|Sheridan|2004}} These transformations are guaranteed to only linearly increase the size of the formula, but introduce new variables. For example, the above formula can be transformed into CNF by adding variables <math>Z_1,\ldots,Z_n</math> as follows:

<math display="block">(Z_1 \vee \ldots \vee Z_n) \wedge
(\neg Z_1 \vee X_1) \wedge (\neg Z_1 \vee Y_1) \wedge
\ldots \wedge 
(\neg Z_n \vee X_n) \wedge (\neg Z_n \vee Y_n). </math>

An [[interpretation (logic)|interpretation]] satisfies this formula only if at least one of the new variables is true. If this variable is <math>Z_i</math>, then both <math>X_i</math> and <math>Y_i</math> are true as well. This means that every [[Model theory|model]] that satisfies this formula also satisfies the original one. On the other hand, only some of the models of the original formula satisfy this one: since the <math>Z_i</math> are not mentioned in the original formula, their values are irrelevant to satisfaction of it, which is not the case in the last formula. This means that the original formula and the result of the translation are [[Equisatisfiability|equisatisfiable]] but not [[logical equivalence|equivalent]].

An alternative translation, the [[Tseitin transformation]], includes also the clauses <math>Z_i \vee \neg X_i \vee \neg Y_i</math>. With these clauses, the formula implies <math>Z_i \equiv X_i \wedge Y_i</math>; this formula is often regarded to "define" <math>Z_i</math> to be a name for <math>X_i \wedge Y_i</math>.