Editing Conjunctive normal form (section)

==Conversion to CNF==
In [[classical logic]] each [[propositional formula]] can be converted to an [[logical equivalence|equivalent]] formula that is in CNF.{{sfn|Howson|2005|page=46}} This transformation is based on rules about [[logical equivalence]]s: [[double negation elimination]], [[De Morgan's laws]], and the [[distributive law]].

=== Basic algorithm ===
The algorithm to compute a CNF-equivalent of a given propositional formula <math>\phi</math> builds upon <math>\lnot \phi</math> in [[Disjunctive normal form|disjunctive normal form (DNF)]]: step 1.<ref name="dnf" /><br/>
Then <math>\lnot \phi_{DNF}</math> is converted to <math>\phi_{CNF}</math> by swapping ANDs with ORs and vice versa while negating all the literals. Remove all <math>\lnot \lnot</math>.{{sfn|Howson|2005|page=46}}

==== Conversion by syntactic means ====
Convert to CNF the propositional formula <math>\phi</math>.

'''Step 1''': Convert its negation to disjunctive normal form.<ref name="dnf">see {{slink|Disjunctive normal form#Conversion to DNF}}</ref> 

<math>\lnot \phi_{DNF} = (C_1 \lor C_2 \lor \ldots \lor C_i \lor \ldots \lor C_m)</math>,{{refn|<math>1 \le m \le</math> [[Disjunctive normal form#max_conjunctions|maximum number of conjunctions]] for <math>\phi</math>}}

where each <math>C_i</math> is a conjunction of literals <math>l_{i1} \land l_{i2} \land \ldots \land l_{in_i}</math>.{{refn|<math>1 \le in_i \le</math> [[Disjunctive normal form#max conjunctions|maximum number of literals]] for <math>\phi</math>}}

'''Step 2''': Negate <math>\lnot \phi_{DNF}</math>.
Then shift <math>\lnot</math> inwards by applying the [[De Morgan's laws#Formal notation|(generalized) De Morgan's equivalences]] until no longer possible.
<math display="block">\begin{align}
\phi &\leftrightarrow \lnot \lnot \phi_{DNF} \\
&= \lnot (C_1 \lor C_2 \lor \ldots \lor C_i \lor \ldots \lor C_m) \\
&\leftrightarrow \lnot C_1 \land \lnot C_2 \land \ldots \land \lnot C_i \land \ldots \land \lnot C_m &&\text{// (generalized) D.M.} 
\end{align}</math>
where<math display="block">\begin{align}
\lnot C_i &= \lnot (l_{i1} \land l_{i2} \land \ldots \land l_{in_i}) \\
&\leftrightarrow (\lnot l_{i1} \lor \lnot l_{i2} \lor \ldots \lor \lnot l_{in_i}) &&\text{// (generalized) D.M.}
\end{align}</math>

'''Step 3''': Remove all double negations.

'''Example'''

Convert to CNF the propositional formula
<math>\phi = ((\lnot (p \land q)) \leftrightarrow (\lnot r \uparrow (p \oplus q)))</math>.{{refn|name=phiverbose|1=<math>\phi</math> = (('''[[Negation|NOT]]''' (p '''[[Logical conjunction|AND]]''' q)) '''[[If and only if|IFF]]''' (('''[[Negation|NOT]]''' r) '''[[Sheffer stroke|NAND]]''' (p '''[[XOR]]''' q)))}}

The (full) DNF equivalent of its negation is<ref name="dnf" /><br/>
<math> \lnot \phi_{DNF} =
(      p \land       q \land       r) \lor
(      p \land       q \land \lnot r) \lor
(      p \land \lnot q \land \lnot r) \lor
(\lnot p \land       q \land \lnot r) </math>

<math display="block">\begin{align}
\phi &\leftrightarrow \lnot \lnot \phi_{DNF} \\
&= \lnot \{
(      p \land       q \land       r) \lor
(      p \land       q \land \lnot r) \lor
(      p \land \lnot q \land \lnot r) \lor
(\lnot p \land       q \land \lnot r) \} \\
&\leftrightarrow
\underline{\lnot( p \land       q \land       r)} \land
\underline{\lnot( p \land       q \land \lnot r)} \land
\underline{\lnot( p \land \lnot q \land \lnot r)} \land
\underline{\lnot(\lnot p  \land q \land \lnot r)} &&\text{// generalized D.M. } \\
&\leftrightarrow
(\lnot p \lor  \lnot q \lor \lnot r) \land
(\lnot p \lor  \lnot q \lor \lnot \lnot r) \land
(\lnot p \lor \lnot \lnot q \lor \lnot \lnot r) \land
(\lnot \lnot p \lor \lnot q \lor \lnot \lnot r) &&\text{// generalized D.M. } (4 \times) \\
&\leftrightarrow
(\lnot p \lor  \lnot q \lor \lnot r) \land
(\lnot p \lor  \lnot q \lor       r) \land
(\lnot p \lor        q \lor       r) \land
(      p \lor \lnot q \lor        r) &&\text{// remove all } \lnot \lnot \\
&= \phi_{CNF}
\end{align}</math>

==== Conversion by semantic means ====
A CNF equivalent of a formula can be derived from its [[truth table]]. Again, consider the formula
<math display="block">\phi = ((\lnot (p \land q)) \leftrightarrow (\lnot r \uparrow (p \oplus q)))</math>.{{refn|name=phiverbose}}

The corresponding [[truth table]] is
{| class="wikitable" style="text-align:center; padding-left: 1.5em;"
! <math>p</math>
! <math>q</math>
! <math>r</math>
! style="background:black"| 
! <math>(</math>
! <math>\lnot</math>
! <math>(p \land q)</math>
! <math>)</math>
! <math>\leftrightarrow</math>
! <math>(</math>
! <math>\lnot r</math>
! <math>\uparrow</math>
! <math>(p \oplus q)</math>
! <math>)</math>
|-
| style="background:lightgreen"|T || style="background:lightgreen"|T || style="background:lightgreen"|T ||style="background:black"| || || F || T || || style="background:papayawhip" | '''F''' || || F || T || F ||
|-
| style="background:lightgreen"|T || style="background:lightgreen"|T || style="background:lightgreen"|F ||style="background:black"| || || F || T || || style="background:papayawhip" | '''F''' || || T || T || F ||
|-
| T || F || T ||style="background:black"| || || T || F || || style="background:papayawhip" | T || || F || T || T ||
|-
| style="background:lightgreen"|T || style="background:lightgreen"|F || style="background:lightgreen"|F ||style="background:black"| || || T || F || || style="background:papayawhip" | '''F''' || || T || F || T ||
|-
| F || T || T ||style="background:black"| || || T || F || || style="background:papayawhip" | T || || F || T || T ||
|-
| style="background:lightgreen"|F || style="background:lightgreen"|T || style="background:lightgreen"|F ||style="background:black"| || || T || F || || style="background:papayawhip" | '''F''' || || T || F || T ||
|-
| F || F || T ||style="background:black"| || || T || F || || style="background:papayawhip" | T || || F || T || F ||
|-
| F || F || F ||style="background:black"| || || T || F || || style="background:papayawhip" | T || || T || T || F ||
|}

A CNF equivalent of <math>\phi</math> is
<math display="block">
(\lnot p \lor \lnot q \lor \lnot r) \land
(\lnot p \lor \lnot q \lor       r) \land
(\lnot p \lor       q \lor       r) \land
(      p \lor \lnot q \lor       r)
</math>

Each disjunction reflects an assignment of variables for which <math>\phi</math> evaluates to F(alse).<br/>
If in such an assignment a variable <math>V</math>
* is T(rue), then the literal is set to <math>\lnot V</math> in the disjunction,
* is F(alse), then the literal is set to <math>V</math> in the disjunction.

===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>.