conjunctive normal form

A logical formula is considered to be in CNF if it is a conjunction of one or more disjunctions of one or more literals. As in disjunctive normal form (DNF), the only propositional operators in CNF are or ($\backslash vee$), and ($\backslash and$), and not ($\backslash neg$). The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.

The following is a context-free grammar for CNF:

: CNF $\backslash ,\; \backslash to\; \backslash ,$ Disjunct $\backslash ,\; \backslash mid\; \backslash ,$ Disjunct $\backslash ,\; \backslash land\; \backslash ,$ CNF

: Disjunct $\backslash ,\; \backslash to\; \backslash ,$ Literal $\backslash ,\; \backslash mid\backslash ,$ Literal $\backslash ,\; \backslash lor\; \backslash ,$ Disjunct

: Literal $\backslash ,\; \backslash to\; \backslash ,$ Variable $\backslash ,\; \backslash mid\; \backslash ,$ $\backslash ,\; \backslash neg\; \backslash ,$ Variable

Where Variable is any variable.

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

• $(A\; \backslash lor\; \backslash neg\; B\; \backslash lor\; \backslash neg\; C)\; \backslash land\; (\backslash neg\; D\; \backslash lor\; E\; \backslash lor\; F\; \backslash lor\; D\; \backslash lor\; F)$
• $(A\; \backslash lor\; B)\; \backslash land\; (C)$
• $(A\; \backslash lor\; B)$
• $(A)$

The following formulas are not in conjunctive normal form:

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

In classical logic each propositional formula can be converted to an equivalent formula that is in CNF.{{sfn|Howson|2005|page=46}} This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.

The algorithm to compute a CNF-equivalent of a given propositional formula $\backslash phi$ builds upon $\backslash lnot\; \backslash phi$ in disjunctive normal form (DNF): step 1.

Then $\backslash lnot\; \backslash phi\_\{DNF\}$ is converted to $\backslash phi\_\{CNF\}$ by swapping ANDs with ORs and vice versa while negating all the literals. Remove all $\backslash lnot\; \backslash lnot$.{{sfn|Howson|2005|page=46}}

Convert to CNF the propositional formula $\backslash phi$.

Step 1: Convert its negation to disjunctive normal form.see {{slink|Disjunctive normal form#Conversion to DNF}}

$\backslash lnot\; \backslash phi\_\{DNF\}\; =\; (C\_1\; \backslash lor\; C\_2\; \backslash lor\; \backslash ldots\; \backslash lor\; C\_i\; \backslash lor\; \backslash ldots\; \backslash lor\; C\_m)$,{{refn|$1\; \backslash le\; m\; \backslash le$ maximum number of conjunctions for $\backslash phi$}}

where each $C\_i$ is a conjunction of literals $l\_\{i1\}\; \backslash land\; l\_\{i2\}\; \backslash land\; \backslash ldots\; \backslash land\; l\_\{in\_i\}$.{{refn|$1\; \backslash le\; in\_i\; \backslash le$ maximum number of literals for $\backslash phi$}}

Step 2: Negate $\backslash lnot\; \backslash phi\_\{DNF\}$.

Then shift $\backslash lnot$ inwards by applying the (generalized) De Morgan's equivalences until no longer possible.

$$\backslash begin\{align\}$$

\phi &\leftrightarrow \lnot \lnot \phi_{DNF} \\

&= \lnot (C_1 \lor C_2 \lor \ldots \lor C_i \lor \ldots \lor C_m) \\

&\leftrightarrow \lnot C_1 \land \lnot C_2 \land \ldots \land \lnot C_i \land \ldots \land \lnot C_m &&\text{// (generalized) D.M.}

\end{align}

where$$\backslash begin\{align\}$$

\lnot C_i &= \lnot (l_{i1} \land l_{i2} \land \ldots \land l_{in_i}) \\

&\leftrightarrow (\lnot l_{i1} \lor \lnot l_{i2} \lor \ldots \lor \lnot l_{in_i}) &&\text{// (generalized) D.M.}

\end{align}

Step 3: Remove all double negations.

Example

Convert to CNF the propositional formula

$\backslash phi\; =\; ((\backslash lnot\; (p\; \backslash land\; q))\; \backslash leftrightarrow\; (\backslash lnot\; r\; \backslash uparrow\; (p\; \backslash oplus\; q)))$.{{refn|name=phiverbose|1=$\backslash phi$ = ((NOT (p AND q)) IFF ((NOT r) NAND (p XOR q)))}}

The (full) DNF equivalent of its negation is

$\backslash lnot\; \backslash phi\_\{DNF\}\; =$

( p \land q \land r) \lor

( p \land q \land \lnot r) \lor

( p \land \lnot q \land \lnot r) \lor

(\lnot p \land q \land \lnot r)

$$\backslash begin\{align\}$$

\phi &\leftrightarrow \lnot \lnot \phi_{DNF} \\

&= \lnot \{

( p \land q \land r) \lor

( p \land q \land \lnot r) \lor

( p \land \lnot q \land \lnot r) \lor

(\lnot p \land q \land \lnot r) \} \\

&\leftrightarrow

\underline{\lnot( p \land q \land r)} \land

\underline{\lnot( p \land q \land \lnot r)} \land

\underline{\lnot( p \land \lnot q \land \lnot r)} \land

\underline{\lnot(\lnot p \land q \land \lnot r)} &&\text{// generalized D.M. } \\

&\leftrightarrow

(\lnot p \lor \lnot q \lor \lnot r) \land

(\lnot p \lor \lnot q \lor \lnot \lnot r) \land

(\lnot p \lor \lnot \lnot q \lor \lnot \lnot r) \land

(\lnot \lnot p \lor \lnot q \lor \lnot \lnot r) &&\text{// generalized D.M. } (4 \times) \\

&\leftrightarrow

(\lnot p \lor \lnot q \lor \lnot r) \land

(\lnot p \lor \lnot q \lor r) \land

(\lnot p \lor q \lor r) \land

( p \lor \lnot q \lor r) &&\text{// remove all } \lnot \lnot \\

&= \phi_{CNF}

\end{align}

A CNF equivalent of a formula can be derived from its truth table. Again, consider the formula

$$\backslash phi\; =\; ((\backslash lnot\; (p\; \backslash land\; q))\; \backslash leftrightarrow\; (\backslash lnot\; r\; \backslash uparrow\; (p\; \backslash oplus\; q)))$$.{{refn|name=phiverbose}}

The corresponding truth table is

A CNF equivalent of $\backslash phi$ is

(\lnot p \lor \lnot q \lor \lnot r) \land

(\lnot p \lor \lnot q \lor r) \land

(\lnot p \lor q \lor r) \land

( p \lor \lnot q \lor r)

Each disjunction reflects an assignment of variables for which $\backslash phi$ evaluates to F(alse).

If in such an assignment a variable $V$

• is T(rue), then the literal is set to $\backslash lnot\; V$ in the disjunction,
• is F(alse), then the literal is set to $V$ in the disjunction.

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

$$(X\_1\; \backslash wedge\; Y\_1)\; \backslash vee\; (X\_2\; \backslash wedge\; Y\_2)\; \backslash vee\; \backslash ldots\; \backslash vee\; (X\_n\; \backslash wedge\; Y\_n)$$

into CNF produces a formula with $2^n$ clauses:

$$(X\_1\; \backslash vee\; X\_2\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_n)\; \backslash wedge\; (Y\_1\; \backslash vee\; X\_2\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_n)\; \backslash wedge\; (X\_1\; \backslash vee\; Y\_2\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_n)\; \backslash wedge\; (Y\_1\; \backslash vee\; Y\_2\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_n)\; \backslash wedge\; \backslash ldots\; \backslash wedge\; (Y\_1\; \backslash vee\; Y\_2\; \backslash vee\; \backslash ldots\; \backslash vee\; Y\_n).$$

Each clause contains either $X\_i$ or $Y\_i$ for each $i$.

There exist transformations into CNF that avoid an exponential increase in size by preserving satisfiability rather than equivalence.{{sfn|Tseitin |1968}}{{sfn|Jackson|Sheridan|2004}} 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 $Z\_1,\backslash ldots,Z\_n$ as follows:

$$(Z\_1\; \backslash vee\; \backslash ldots\; \backslash vee\; Z\_n)\; \backslash 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 $Z\_i$, then both $X\_i$ and $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 $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 $Z\_i\; \backslash vee\; \backslash neg\; X\_i\; \backslash vee\; \backslash neg\; Y\_i$. With these clauses, the formula implies $Z\_i\; \backslash equiv\; X\_i\; \backslash wedge\; Y\_i$; this formula is often regarded to "define" $Z\_i$ to be a name for $X\_i\; \backslash wedge\; Y\_i$.

Consider a propositional formula with $n$ variables, $n\; \backslash ge\; 1$.

There are $2n$ possible literals: $L\; =\; \backslash \{\; p\_1,\; \backslash lnot\; p\_1,\; p\_2,\; \backslash lnot\; p\_2,\; \backslash ldots,\; p\_n,\; \backslash lnot\; p\_n\backslash \}$.

$L$ has $(2^\{2n\}\; -1)$ non-empty subsets.{{refn|$\backslash left|\backslash mathcal\{P\}(L)\backslash right|\; =\; 2^\{2n\}$}}

This is the maximum number of disjunctions a CNF can have.{{refn|name=noreps|It is assumed that repetitions and variations (like $(a\; \backslash land\; b)\; \backslash lor\; (b\; \backslash land\; a)\; \backslash lor\; (a\; \backslash land\; b\; \backslash land\; b)$) based on the commutativity and associativity of $\backslash lor$ and $\backslash land$ do not occur.}}

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

Example

Consider a formula with two variables $p$ and $q$.

The longest possible CNF has $2^\{(2\; \backslash times\; 2)\}\; -1\; =\; 15$ disjunctions:{{refn|name=noreps}}

\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}

This formula is a contradiction. It can be simplified to $(\backslash neg\; p\; \backslash land\; p)$ or to $(\backslash neg\; q\; \backslash land\; q)$, which are also contradictions, as well as valid CNFs.

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,{{refn|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}} 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 $X\_1\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_k\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_n$ by two conjuncts $X\_1\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_\{k-1\}\; \backslash vee\; Z$ and $\backslash neg\; Z\; \backslash vee\; X\_k\; \backslash lor\; \backslash ldots\; \backslash vee\; X\_n$ with {{mvar|Z}} a new variable, and repeating as often as necessary.

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

See below for an example.

To convert first-order logic to CNF:{{sfn|Russel|Norvig|2010|pages=345-347|loc=9.5.1 Conjunctive normal form for first-order logic}}

1. Convert to negation normal form.
2. Eliminate implications and equivalences: repeatedly replace $P\; \backslash rightarrow\; Q$ with $\backslash lnot\; P\; \backslash lor\; Q$; replace $P\; \backslash leftrightarrow\; Q$ with $(P\; \backslash lor\; \backslash lnot\; Q)\; \backslash land\; (\backslash lnot\; P\; \backslash lor\; Q)$. Eventually, this will eliminate all occurrences of $\backslash rightarrow$ and $\backslash leftrightarrow$.
3. Move NOTs inwards by repeatedly applying De Morgan's law. Specifically, replace $\backslash lnot\; (P\; \backslash lor\; Q)$ with $(\backslash lnot\; P)\; \backslash land\; (\backslash lnot\; Q)$; replace $\backslash lnot\; (P\; \backslash land\; Q)$ with $(\backslash lnot\; P)\; \backslash lor\; (\backslash lnot\; Q)$; and replace $\backslash lnot\backslash lnot\; P$ with $P$; replace $\backslash lnot\; (\backslash forall\; x\; P(x))$ with $\backslash exists\; x\; \backslash lnot\; P(x)$; $\backslash lnot\; (\backslash exists\; x\; P(x))$ with $\backslash forall\; x\; \backslash lnot\; P(x)$. After that, a $\backslash lnot$ may occur only immediately before a predicate symbol.
4. Standardize variables
5. For sentences like $(\backslash forall\; x\; P(x))\; \backslash lor\; (\backslash exists\; x\; Q(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, $\backslash forall\; x\; [\backslash exists\; y\; \backslash mathrm\{Animal\}(y)\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; y)]\; \backslash lor\; [\backslash exists\; y\; \backslash mathrm\{Loves\}(y,\; x)]$ is renamed to $\backslash forall\; x\; [\backslash exists\; y\; \backslash mathrm\{Animal\}(y)\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; y)]\; \backslash lor\; [\backslash exists\; z\; \backslash mathrm\{Loves\}(z,x)]$.
6. Skolemize the statement
7. Move quantifiers outwards: repeatedly replace $P\; \backslash land\; (\backslash forall\; x\; Q(x))$ with $\backslash forall\; x\; (P\; \backslash land\; Q(x))$; replace $P\; \backslash lor\; (\backslash forall\; x\; Q(x))$ with $\backslash forall\; x\; (P\; \backslash lor\; Q(x))$; replace $P\; \backslash land\; (\backslash exists\; x\; Q(x))$ with $\backslash exists\; x\; (P\; \backslash land\; Q(x))$; replace $P\; \backslash lor\; (\backslash exists\; x\; Q(x))$ with $\backslash exists\; x\; (P\; \backslash lor\; Q(x))$. These replacements preserve equivalence, since the previous variable standardization step ensured that $x$ doesn't occur in $P$. After these replacements, a quantifier may occur only in the initial prefix of the formula, but never inside a $\backslash lnot$, $\backslash land$, or $\backslash lor$.
8. Repeatedly replace $\backslash forall\; x\_1\; \backslash ldots\; \backslash forall\; x\_n\; \backslash ;\; \backslash exists\; y\; \backslash ;\; P(y)$ with $\backslash forall\; x\_1\; \backslash ldots\; \backslash forall\; x\_n\; \backslash ;\; P(f(x\_1,\backslash ldots,x\_n))$, where $f$ is a new $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.
9. Drop all universal quantifiers.
10. Distribute ORs inwards over ANDs: repeatedly replace $P\; \backslash lor\; (Q\; \backslash land\; R)$ with $(P\; \backslash lor\; Q)\; \backslash land\; (P\; \backslash 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 $\{\backslash color\{red\}\{\backslash text\{red\}\}\}$):

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

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

• Algebraic normal form
• Conjunction/disjunction duality
• Disjunctive normal form
• Horn clause – A Horn clause is a disjunctive clause (a disjunction of literals) with at most one positive, i.e. unnegated, literal.
• Quine–McCluskey algorithm

{{reflist}}

{{refbegin}}

• {{Cite book

|last=Andrews

|first=Peter B.

|year=2013

|title=An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof

|publisher=Springer

|isbn=978-9401599344

}}

• {{cite book

|last=Howson

|first=Colin

|author-link=Colin Howson

|title=Logic with trees: an introduction to symbolic logic

|url=https://books.google.com/books?id=Y4WGAgAAQBAJ&q=%22conjunctive+normal+form%22

|date=11 October 2005

|orig-date=1997

|publisher=Routledge

|isbn=978-1-134-78550-6

}}

• {{Cite conference

|last1=Jackson

|first1=Paul

|last2=Sheridan

|first2=Daniel

|url=https://homepages.inf.ed.ac.uk/pbj/papers/sat04-bc-conv.pdf

|title=Clause Form Conversions for Boolean Circuits

|editor1-last=Hoos

|editor1-first=Holger H.

|editor2-last=Mitchell

|editor2-first=David G.

|book-title=Theory and Applications of Satisfiability Testing

|conference=7th International Conference on Theory and Applications of Satisfiability Testing, SAT

|conference-url=https://link.springer.com/book/10.1007/11527695

|date=10 May 2004

|location=Vancouver, BC, Canada

|pages=183{{ndash}}198

|series=Revised Selected Papers. Lecture Notes in Computer Science

|volume=3542

|publisher=Springer 2005

|doi=10.1007/11527695_15

|isbn=978-3-540-31580-3

}}

• {{cite book

|last1=Kleine Büning

|first1=Hans

|last2=Lettmann

|first2=Theodor

|date=28 August 1999

|title=Propositional Logic: Deduction and Algorithms

|url=https://books.google.com/books?id=3oJE9yczr3EC&q=%22conjunctive+normal+form%22

|publisher=Cambridge University Press

|isbn=978-0-521-63017-7

}}

• {{Cite book

|editor1-last=Russel

|editor1-first=Stuart

|editor1-link=Stuart J. Russell

|editor2-last=Norvig

|editor2-first=Peter

|editor2-link=Peter Norvig

|date=2010

|orig-date=1995

|title=Artificial Intelligence : A Modern Approach

|url=https://people.engr.tamu.edu/guni/csce421/files/AI_Russell_Norvig.pdf

|edition=3rd

|publisher=Prentice Hall

|location=Upper Saddle River, NJ

|isbn=978-0-13-604259-4

|archive-url=https://web.archive.org/web/20170831090316/https://pdfs.semanticscholar.org/bef0/731f247a1d01c9e0ff52f2412007c143899d.pdf

|archive-date=31 August 2017

|url-status=live

}}

• {{Cite book

|last=Tseitin

|first=Grigori S.

|author-link=Grigori Tseitin

|year=1968

|chapter=On the Complexity of Derivation in Propositional Calculus

|chapter-url=http://www.decision-procedures.org/handouts/Tseitin70.pdf

|editor-last=Slisenko

|editor-first=A.O.

|title=Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian)

|pages=115–125

|publisher=Steklov Mathematical Institute

}}

• {{cite book

|last=Whitesitt

|first=J. Eldon

|date=24 May 2012

|orig-year=1961

|title=Boolean Algebra and Its Applications

|url=https://books.google.com/books?id=20Un1T78GlMC&q=%22conjunctive+normal+form%22

|publisher=Courier Corporation

|isbn=978-0-486-15816-7

}}

{{refend}}

• {{springer

|title=Conjunctive normal form

|id=p/c025090

}}

• {{Cite web

|url=https://www.mathematik.uni-marburg.de/~thormae/lectures/ti1/code/normalform/index.html

|title=Java tool for converting a truth table into CNF and DNF

|at=[https://www.uni-marburg.de/en/ Universität Marburg]

|access-date=31 December 2023

}}

Category:Normal forms (logic)

Category:Knowledge compilation

{{Normal forms in logic}}