Conjunctive Normal Form (Propositional Logic)

Definition

Conjunctive Normal Form (Propositional Logic)

A propositional formula is in conjunctive normal form (CNF) if it is a conjunction of disjunctions of literals — a conjunction of clauses:

$$\underset{i=1}{\overset{n}{\bigwedge }}\underset{j=1}{\overset{m_i}{\bigvee }}{L}_{ij},$$

where each $L_{ij}$ is a literal, i.e. an atom or a negated atom. The degenerate cases count as well: a single clause ($p\vee q$), a single literal ($\neg p$), and a single atom ($p$) are all in CNF. Examples:

$$(\neg a\vee b)\wedge (a\vee \neg c\vee d)\wedge \neg b$$

Existence

Definition

Normal Form Existence (Propositional Logic)

Every propositional formula $F$ has an equivalent formula in conjunctive normal form and an equivalent formula in disjunctive normal form:

$$\forall F:\exists F_{\wedge }:F\equiv F_{\wedge }\in \mathrm{CNF},\exists F_{\vee }:F\equiv F_{\vee }\in \mathrm{DNF}.$$

The literature usually states this as an unremarkable proposition rather than a named theorem; “normal form theorem” and “CNF–DNF existence theorem” are the common labels.

Link to original

Transformation

Every formula has an equivalent CNF (normal form existence). Rewriting applies the De Morgan’s rules, double negation elimination, and distributivity to subformulas $A,B,A_1,\dots ,A_m$:

$$\begin{array}{rl}A\leftrightarrow B& \equiv (\neg A\vee B)\wedge (\neg B\vee A)\\ A\to B& \equiv \neg A\vee B\\ \neg (A\wedge B)& \equiv \neg A\vee \neg B\\ \neg (A\vee B)& \equiv \neg A\wedge \neg B\\ \neg \neg A& \equiv A\\ (A_1\wedge \cdots \wedge A_m)\vee B& \equiv (A_1\vee B)\wedge \cdots \wedge (A_m\vee B)\end{array}$$

Worked transformation

$$\begin{array}{rl}F& =\neg ((p\to q)\wedge (p\wedge q\to r)\to (p\to r))\\ & \equiv \neg (\neg ((p\to q)\wedge (p\wedge q\to r))\vee (p\to r))\\ & \equiv \neg (\neg ((\neg p\vee q)\wedge (p\wedge q\to r))\vee (p\to r))\\ & \equiv \neg (\neg ((\neg p\vee q)\wedge (\neg (p\wedge q)\vee r))\vee (p\to r))\\ & \equiv \neg (\neg ((\neg p\vee q)\wedge (\neg (p\wedge q)\vee r))\vee (\neg p\vee r))\\ & \equiv \neg (\neg ((\neg p\vee q)\wedge (\neg p\vee \neg q\vee r))\vee (\neg p\vee r))\\ & \equiv \neg \neg ((\neg p\vee q)\wedge (\neg p\vee \neg q\vee r))\wedge \neg (\neg p\vee r)\\ & \equiv ((\neg p\vee q)\wedge (\neg p\vee \neg q\vee r))\wedge \neg (\neg p\vee r)\\ & \equiv ((\neg p\vee q)\wedge (\neg p\vee \neg q\vee r))\wedge (p\wedge \neg r)\\ & \equiv (\neg p\vee q)\wedge (\neg p\vee \neg q\vee r)\wedge p\wedge \neg r\end{array}$$

Exponential Blow-up

Warning

Some formulas have only exponentially large equivalent CNFs, e.g.

$$p_1\leftrightarrow (p_2\leftrightarrow (p_3\leftrightarrow (p_4\leftrightarrow (p_5\leftrightarrow p_6))))$$

The blow-up is avoided by naming (the definitional transformation), which preserves satisfiability rather than equivalence.