Editing Conjunctive normal form (section)

== Maximum number of disjunctions ==
<span id="max_disjunctions"></span>
Consider a propositional formula with <math>n</math> variables, <math>n \ge 1</math>.

There are <math>2n</math> possible literals: <math>L = \{ p_1, \lnot p_1, p_2, \lnot p_2, \ldots, p_n, \lnot p_n\}</math>.

<math>L</math> has <math>(2^{2n} -1)</math> non-empty subsets.{{refn|<math>\left|\mathcal{P}(L)\right| = 2^{2n}</math>}}

This is the maximum number of disjunctions a CNF can have.{{refn|name=noreps|It is assumed that repetitions and variations (like <math>(a \land b) \lor (b \land a) \lor (a \land b \land b)</math>) based on the [[Commutative property|commutativity]] and [[Associative property|associativity]] of <math>\lor</math> and <math>\land</math> do not occur.}}

All truth-functional combinations can be expressed with <math>2^{n}</math> disjunctions, one for each row of the truth table.<br/>In the example below they are underlined.

'''Example'''

Consider a formula with two variables <math>p</math> and <math>q</math>.

The longest possible CNF has <math>2^{(2 \times 2)} -1 = 15</math> disjunctions:{{refn|name=noreps}}
<math display="block"> 
\begin{array}{lcl}
(\lnot p) \land (p) \land (\lnot q) \land (q) \land \\
(\lnot p \or       p) \land
\underline{(\lnot p \or \lnot q)} \land
\underline{(\lnot p \or       q)} \land
\underline{(      p \or \lnot q)} \land
\underline{(      p \or       q)} \land
(\lnot q \or       q) \land \\
(\lnot p \or       p \or \lnot q) \land	
(\lnot p \or       p \or       q) \land	
(\lnot p \or \lnot q \or       q) \land	
(      p \or \lnot q \or       q) \land \\
(\lnot p \or       p \or \lnot q \or q)
\end{array}</math>

This formula is a [[contradiction]]. It can be simplified to <math>(\neg p \land p)</math> or to <math>(\neg q \land q)</math>, which are also contradictions, as well as valid CNFs.