Conjunctive normal form

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

All conjunctions of literals and all disjunctions of literals are in CNF, as they can be seen as conjunctions of one-literal clauses and conjunctions of a single clause, respectively. As in the disjunctive normal form (DNF), the only propositional connectives a formula in CNF can contain are and, or, and not. The not operator can only be used as part of a literal, which means that it can only precede a propositional variable or a predicate symbol.

In automated theorem proving, the notion "clausal normal form" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals.

Examples and non-examples

All of the following formulas in the variables A, B, C, D, E, and F are in conjunctive normal form:

• ${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)}$
• ${\displaystyle (A\lor B)\land C}$
• ${\displaystyle A\lor B}$
• ${\displaystyle A}$

The third formula is in conjunctive normal form because it is viewed as a "conjunction" with just one conjunct, namely the clause ${\displaystyle A\lor B}$. Incidentally, the last two formulas are also in disjunctive normal form.

The following formulas are not in conjunctive normal form:

• ${\displaystyle \neg (B\lor C)}$, since an OR is nested within a NOT
• ${\displaystyle (A\land B)\lor C}$
• ${\displaystyle A\land (B\lor (D\land E))}$, since an AND is nested within an OR

Every formula can be equivalently written as a formula in conjunctive normal form. In particular this is the case for the three non-examples just mentioned; they are respectively equivalent to the following three formulas, which are in conjunctive normal form:

• ${\displaystyle \neg B\land \neg C}$
• ${\displaystyle (A\lor C)\land (B\lor C)}$
• ${\displaystyle A\land (B\lor D)\land (B\lor E).}$

Conversion into CNF

[1]Every propositional formula can be converted into an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.

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 following non-CNF formula into CNF produces a formula with ${\displaystyle 2^{n}}$ clauses:

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

In particular, the generated formula is:

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

This formula contains ${\displaystyle 2^{n}}$ clauses; 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.[2][3] 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 \cdots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \cdots \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, includes also 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}}$.

First-order logic

In first order logic, conjunctive normal form can be taken further to yield the clausal normal form of a logical formula, which can be then used to perform first-order resolution. In resolution-based automated theorem-proving, a CNF formula

${\displaystyle (}$

${\displaystyle l_{11}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{1n_{1}}}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \ldots }$

${\displaystyle \land }$

${\displaystyle (}$

${\displaystyle l_{m1}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{mn_{m}}}$

${\displaystyle )}$

, with ${\displaystyle l_{ij}}$ literals, is commonly represented as a set of sets

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle l_{11}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{1n_{1}}}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle l_{m1}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{mn_{m}}}$

${\displaystyle \}}$

${\displaystyle \}}$

.

See below for an example.

Computational complexity

An important set of problems in computational complexity involves finding assignments to the variables of a boolean formula expressed in Conjunctive Normal Form, such that the formula is true. The k-SAT problem is the problem of finding a satisfying assignment to a boolean formula expressed in CNF in which each disjunction contains at most k variables. 3-SAT is NP-complete (like any other k-SAT problem with k>2) while 2-SAT is known to have solutions in polynomial time. As a consequence,[4] the task of converting a formula into a DNF, preserving satisfiability, is NP-hard; dually, converting into CNF, preserving validity, is also NP-hard; hence equivalence-preserving conversion into DNF or CNF is again NP-hard.

Typical problems in this case involve formulas in "3CNF": conjunctive normal form with no more than three variables per conjunct. Examples of such formulas encountered in practice can be very large, for example with 100,000 variables and 1,000,000 conjuncts.

A formula in CNF can be converted into an equisatisfiable formula in "kCNF" (for k≥3) by replacing each conjunct with more than k variables ${\displaystyle X_{1}\vee \cdots \vee X_{k}\vee \cdots \vee X_{n}}$ by two conjuncts ${\displaystyle X_{1}\vee \cdots \vee X_{k-1}\vee Z}$ and ${\displaystyle \neg Z\vee X_{k}\cdots \vee X_{n}}$ with Z a new variable, and repeating as often as necessary.

Converting from first-order logic

To convert first-order logic to CNF:[1]

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)}$.

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}}}}$):

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

by 1.1

${\displaystyle \forall x}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle {\color {red}{\forall y}}}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

by 1.1

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

by 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle \color {red}\lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

by 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

by 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}z}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

${\displaystyle )}$

by 2

${\displaystyle \forall x}$

${\displaystyle \exists z}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

by 3.1

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists z}}}$

${\displaystyle \exists y}$

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

by 3.1

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

by 3.2

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

by 4

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle (}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle )}$

by 5

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle \}}$

${\displaystyle \}}$

(clause representation)

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.

Notes

1. Artificial Intelligence: A modern Approach Archived 2017-08-31 at the Wayback Machine [1995...] Russell and Norvig
2. Tseitin (1968)
3. Jackson and Sheridan (2004)
4. since one way to check a CNF for satisfiability is to convert it into a DNF, the satisfiability of which can be checked in linear time

See also

• Algebraic normal form
• Disjunctive normal form
• Horn clause
• Quine–McCluskey algorithm

References

• J. Eldon Whitesitt (24 May 2012). Boolean Algebra and Its Applications. Courier Corporation. ISBN 978-0-486-15816-7.
• Hans Kleine Büning; Theodor Lettmann (28 August 1999). Propositional Logic: Deduction and Algorithms. Cambridge University Press. ISBN 978-0-521-63017-7.
• Paul Jackson, Daniel Sheridan: Clause Form Conversions for Boolean Circuits. In: Holger H. Hoos, David G. Mitchell (Eds.): Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3542, Springer 2005, pp. 183–198
• G.S. Tseitin: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian), pp. 115–125. Steklov Mathematical Institute (1968)

External links

• "Conjunctive normal form", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• Java applet for converting to CNF and DNF, showing laws used