Editing Conjunctive normal form (section)

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