Conjunctive normal form

The algorithm to compute a CNF-equivalent of a given propositional formula ${\displaystyle \phi }$ builds upon ${\displaystyle \lnot \phi }$ in disjunctive normal form (DNF): step 1.^[2] Then ${\displaystyle \lnot \phi _{DNF}}$ is converted to ${\displaystyle \phi _{CNF}}$ by swapping ANDs with ORs and vice versa while negating all the literals. Remove all ${\displaystyle \lnot \lnot }$.^[1]

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

$${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \ldots \vee (X_{n}\wedge Y_{n})}$$

into CNF produces a formula with ${\displaystyle 2^{n}}$ clauses:

$${\displaystyle (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}).}$$

Each clause contains either ${\displaystyle X_{i}}$ or ${\displaystyle Y_{i}}$ for each ${\displaystyle i}$.

There exist transformations into CNF that avoid an exponential increase in size by preserving satisfiability rather than equivalence.^[6][7] 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 ${\displaystyle Z_{1},\ldots ,Z_{n}}$ as follows:

$${\displaystyle (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}).}$$

An interpretation satisfies this formula only if at least one of the new variables is true. If this variable is ${\displaystyle Z_{i}}$, then both ${\displaystyle X_{i}}$ and ${\displaystyle Y_{i}}$ are true as well. This means that every 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 ${\displaystyle Z_{i}}$ 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 equisatisfiable but not equivalent.

An alternative translation, the Tseitin transformation, also includes the clauses ${\displaystyle Z_{i}\vee \neg X_{i}\vee \neg Y_{i}}$. With these clauses, the formula implies ${\displaystyle Z_{i}\equiv X_{i}\wedge Y_{i}}$; this formula is often regarded to "define" ${\displaystyle Z_{i}}$ to be a name for ${\displaystyle X_{i}\wedge Y_{i}}$.

To convert first-order logic to CNF:^[12]

1. Convert to negation normal form.
   1. Eliminate implications and equivalences: repeatedly replace ${\displaystyle P\rightarrow Q}$ with ${\displaystyle \lnot P\lor Q}$; replace ${\displaystyle P\leftrightarrow Q}$ with ${\displaystyle (P\lor \lnot Q)\land (\lnot P\lor Q)}$. Eventually, this will eliminate all occurrences of ${\displaystyle \rightarrow }$ and ${\displaystyle \leftrightarrow }$.
   2. Move NOTs inwards by repeatedly applying De Morgan's law. Specifically, replace ${\displaystyle \lnot (P\lor Q)}$ with ${\displaystyle (\lnot P)\land (\lnot Q)}$; replace ${\displaystyle \lnot (P\land Q)}$ with ${\displaystyle (\lnot P)\lor (\lnot Q)}$; and replace ${\displaystyle \lnot \lnot P}$ with ${\displaystyle P}$; replace ${\displaystyle \lnot (\forall xP(x))}$ with ${\displaystyle \exists x\lnot P(x)}$; ${\displaystyle \lnot (\exists xP(x))}$ with ${\displaystyle \forall x\lnot P(x)}$. After that, a ${\displaystyle \lnot }$ may occur only immediately before a predicate symbol.
2. Standardize variables
   1. For sentences like ${\displaystyle (\forall xP(x))\lor (\exists xQ(x))}$ which use the same variable name twice, change the name of one of the variables. This avoids confusion later when dropping quantifiers. For example, ${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]}$ is renamed to ${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists z\mathrm {Loves} (z,x)]}$.
3. Skolemize the statement
   1. Move quantifiers outwards: repeatedly replace ${\displaystyle P\land (\forall xQ(x))}$ with ${\displaystyle \forall x(P\land Q(x))}$; replace ${\displaystyle P\lor (\forall xQ(x))}$ with ${\displaystyle \forall x(P\lor Q(x))}$; replace ${\displaystyle P\land (\exists xQ(x))}$ with ${\displaystyle \exists x(P\land Q(x))}$; replace ${\displaystyle P\lor (\exists xQ(x))}$ with ${\displaystyle \exists x(P\lor Q(x))}$. These replacements preserve equivalence, since the previous variable standardization step ensured that ${\displaystyle x}$ doesn't occur in ${\displaystyle P}$. After these replacements, a quantifier may occur only in the initial prefix of the formula, but never inside a ${\displaystyle \lnot }$, ${\displaystyle \land }$, or ${\displaystyle \lor }$.
   2. Repeatedly replace ${\displaystyle \forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)}$ with ${\displaystyle \forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))}$, where ${\displaystyle f}$ is a new ${\displaystyle n}$-ary function symbol, a so-called "Skolem function". This is the only step that preserves only satisfiability rather than equivalence. It eliminates all existential quantifiers.
4. Drop all universal quantifiers.
5. Distribute ORs inwards over ANDs: repeatedly replace ${\displaystyle P\lor (Q\land R)}$ with ${\displaystyle (P\lor Q)\land (P\lor R)}$.

Example

As an example, the formula saying "Anyone who loves all animals, is in turn loved by someone" is converted into CNF (and subsequently into clause form in the last line) as follows (highlighting replacement rule redexes in ${\displaystyle {\color {red}{\text{red}}}}$):

Informally, the Skolem function ${\displaystyle g(x)}$ can be thought of as yielding the person by whom ${\displaystyle x}$ is loved, while ${\displaystyle f(x)}$ yields the animal (if any) that ${\displaystyle x}$ doesn't love. The 3rd last line from below then reads as "${\displaystyle x}$ doesn't love the animal ${\displaystyle f(x)}$, or else ${\displaystyle x}$ is loved by ${\displaystyle g(x)}$".

The 2nd last line from above, ${\displaystyle (\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))}$, is the CNF.