Conjunctive normal form (propositional logic)

A propositional formula is in conjunctive normal form if it is a conjunction of disjunctions of negated and non-negated variables. Conjunctive normal form is a normal form which can be used both for modelling and computing 1-assignments in a syntactic fashion.

Formal definition

For every $i \in \mathbf N$, the formulas $X_i$ and $\neg X_i$ are literals. A formula is in conjunctive normal form (CNF) if it is of the form \begin{align} \bigwedge_{i<m}\bigvee_{j<n_i} L_i^j \end{align} where $m, n_i \in \mathbf N$ and the $L_i^j$s are literals.

Example When human-readable notation is adopted, then $(X_0 \vee \neg X_1) \wedge (X_1 \vee \neg X_2)$ is in CNF, but neither $\top$ nor $(X_0 \wedge X_1) \wedge \neg X_2$ are in CNF. When human-readable notation is not adopted, then the first formula is not in CNF, but the formula $\bigwedge(\bigvee(X_0, \neg X_1), \bigvee(X_1, \neg X_2))$.

Example Here are interesting extreme examples. $\bigwedge()$ is in CNF and equivalent to $\top$; $\bigwedge(\bigvee())$ is in conjunctive normal form and equivalent to $\bot$; $\bigwedge(\bigvee(X_i))$ is in conjunctive normal form and equivalent to $X_i$; $\bigwedge(\bigvee(\neg X_i))$ is in conjunctive normal form and equivalent to $\neg X_i$.

Laws for working with CNF

When working with formulas in CNF it is important to have rules at hand that describe how disjunction and conjunction can be applied to formulas in CNF.-Negation cannot be dealt with as easily as with conjunction and disjunction.

Lemma For all $m, n \in \mathbf N$, \begin{align} \label{conjunction} \bigwedge_{i<m}{X_i} \wedge \bigwedge_{i<n}X_{m+i} & \SemEquiv \bigwedge_{i<m+n}X_i \enspace,\\ \bigvee_{i<m}{X_i} \vee \bigvee_{i<n}X_{m+i} \label{disjunctionn} & \SemEquiv \bigvee_{i<m+n}X_i \enspace,\\ \label{disjunction} \bigwedge_{i<m}{X_i} \vee \bigwedge_{j<n}X_{m+j} & \SemEquiv \bigwedge_{i<m, j<n} (X_i \vee X_{m+j}) \enspace. \end{align}

Conversion into conjunctive normal form

Theorem Every propositional formula is equivalent to a formula in conjunctive normal form.

Proof To prove this, first recall that every propositional formula is equivalent to a formula in negation normal form. So it remains to be shown that every formula in negation normal form is equivalent to a formula in conjunctive normal form.

This is proved by induction in the following.

Base case. If $\varphi = \bot$, then $\bigwedge(\bigvee()) \SemEquiv \varphi$. If $\varphi = \top$, then $\bigwedge() \SemEquiv \varphi$. If $\varphi = X_i$ or $\varphi = \neg X_i$ for some $i \in \mathbf N$, then $\bigwedge(\bigvee(\varphi)) \SemEquiv \varphi$.

Inductive step. First, assume $\varphi_0$ and $\varphi_1$ are formulas in NNF which are equivalent to $\bigwedge_{i<m}\psi_i$ and $\bigwedge_{i<n}\psi_{m+i}$, respectively, in CNF. We want to show that $\varphi_0 \wedge \varphi_1$ is equivalent to a formula in CNF. We have: \begin{align} \varphi_0 \wedge \varphi_1 & \SemEquiv \bigwedge_{i<m}\psi_i \wedge \bigwedge_{i<n}\psi_{m+i} && \text{congruence lemma}\\ & \SemEquiv \bigwedge_{i<m+n}\psi_i && \text{by (\ref{conjunction})} \end{align} The last formula is in CNF.

Second, assume $\varphi_0$ and $\varphi_1$ are formulas in NNF which are equivalent to $\bigwedge_{i<m}\bigvee_{j<n_i}L_i^j$ and $\bigwedge_{k<p}\bigvee_{l<q_k}M_k^l$, respectively, in CNF. We want to show that $\varphi_0 \vee \varphi_1$ is equivalent to a formula in CNF. We have: \begin{align} \varphi_0 \vee \varphi_1 & \SemEquiv \bigwedge_{i<m}\bigvee_{j<n_i}L_i^j \vee \bigwedge_{k<p}\bigvee_{l<q_k}M_k^l && \text{congruence lemma}\\ & \SemEquiv \bigwedge_{i<m, k<p} \left(\bigvee_{j<n_i} L_i^j \vee \bigvee_{l < q_k} M_k^l\right)&& \text{by (\ref{disjunction})}\\ & \SemEquiv \bigwedge_{i<m, k<p} \bigvee(L_i^0, \dots, L_i^{n_i-1}, M_k^0, \dots, M_k^{q_k-1}) && \text{by (\ref{disjunctionn})} \end{align} The last formula is in CNF.

This concludes the proof.

Example Here is a very simple example, where we start right from a formula in NNF: $(X_0 \wedge \neg X_1) \vee (\neg X_2 \wedge X_3)$.

In the base step, we obtain four formulas in CNF: $\bigwedge(\bigvee(X_0))$, $\bigwedge(\bigvee(\neg X_1))$, $\bigwedge(\bigvee(\neg X_2))$, and $\bigwedge(\bigvee(X_3))$.

In the second step, we are twice in the same situation as in the first case of the inductive step. We obtain $\bigwedge(\bigvee(X_0), \bigvee(\neg X_1))$ and $\bigwedge(\bigvee(\neg X_2), \bigvee(X_3))$, respectively.

Finally, we are in the same situation as in the second case of the inductive step. We obtain $$\bigwedge(\bigvee(X_0, \neg X_2), \bigvee(X_0, X_3), \bigvee(\neg X_1, \neg X_2), \bigvee(\neg X_1, X_3)) \enspace.$$

Further remarks

The notation for CNF using $\bigwedge$ and $\bigvee$ is somewhat clumsy. A more handy notation is clausal notation.

It is indeed true that various modelling tasks can be accomplished in CNF, see, for instance, the modelling of sudoku and the modelling of computations.