1.4 Normal Forms

Normal forms are standard shapes for propositional formulas, and they are useful because they make formulas easier to compare, transform, and process by algorithms.

Literals and Clauses

A literal is either a propositional variable or the negation of a propositional variable.

Thus the following are literals:

The formula:

is not a literal, because the negation is applied to a compound formula rather than directly to a variable.

A clause is a disjunction of literals. For example:

is a clause.

A term is a conjunction of literals. For example:

is a term.

These words are used to describe the two most common normal forms.

Definition 1.26 (Conjunctive Normal Form)

A formula is in conjunctive normal form, or CNF, if it is a conjunction of clauses.

Equivalently, a CNF formula has the form:

where each $C_i$ is a disjunction of literals.

For example:

is in conjunctive normal form.

A single clause is also regarded as a CNF formula, since it is a conjunction with one conjunct.

Definition 1.27 (Disjunctive Normal Form)

A formula is in disjunctive normal form, or DNF, if it is a disjunction of terms.

Equivalently, a DNF formula has the form:

where each $T_i$ is a conjunction of literals.

For example:

is in disjunctive normal form.

A single term is also regarded as a DNF formula, since it is a disjunction with one disjunct.

Example 1.28

The formula:

is in CNF, because it is a conjunction of two clauses.

The formula:

is in DNF, because it is a disjunction of two terms.

The formula:

is in CNF, since it may be read as:

The same formula is not in DNF as written, because one conjunct contains a disjunction.

Negation Normal Form

Before converting a formula to CNF or DNF, it is useful to first put it into a simpler intermediate form.

A formula is in negation normal form if negation occurs only directly in front of propositional variables.

For example:

is in negation normal form.

The formula:

is not in negation normal form, because the negation is applied to a compound formula.

Lemma 1.29 (Conversion to Negation Normal Form)

Every propositional formula is logically equivalent to a formula in negation normal form.

Proof

The proof is by structural induction on formulas.

If the formula is a variable, then it is already in negation normal form.

If the formula has the form $¬A$, then we consider the structure of $A$. If $A$ is a variable, then $¬A$ is already in negation normal form. If $A$ is itself a negation, then double negation removes two negation signs:

If $A$ is a conjunction or disjunction, then De Morgan laws move the negation inward:

and:

If $A$ contains implication or biconditional, those connectives are first eliminated using:

and:

By repeatedly applying these equivalences, every negation is pushed inward until it applies only to variables.

Conversion Rules

The usual conversion to CNF or DNF proceeds in stages.

First, eliminate biconditionals:

Second, eliminate implications:

Third, push negations inward using:

After these steps, the formula is in negation normal form.

To obtain CNF, distribute disjunction over conjunction:

To obtain DNF, distribute conjunction over disjunction:

Example 1.30 (Conversion to CNF)

Convert the formula:

to CNF.

First eliminate the implication:

Thus:

Now push the negation inward:

Hence:

Now distribute $\lor$ over $\land$:

Therefore a CNF form is:

Example 1.31 (Conversion to DNF)

Convert the same formula:

to DNF.

As above:

This is already in DNF, since it is a disjunction of terms:

The literal $r$ is regarded as a term with one literal.

Lemma 1.32 (Existence of CNF and DNF)

Every propositional formula is logically equivalent to a formula in conjunctive normal form and to a formula in disjunctive normal form.

Proof

First convert the formula to negation normal form. This removes implications and biconditionals and ensures that every negation applies only to a variable.

For CNF, repeatedly distribute disjunction over conjunction:

Each application moves conjunctions outward until the outermost structure is a conjunction of clauses.

For DNF, repeatedly distribute conjunction over disjunction:

Each application moves disjunctions outward until the outermost structure is a disjunction of terms.

Since formulas are finite, the process terminates after finitely many steps.

Normal Forms from Truth Tables

Normal forms can also be obtained directly from a truth table.

To construct a DNF formula, take each row in which the formula is true. For each such row, write a term that describes exactly that row. Then take the disjunction of all such terms.

For example, suppose a formula in variables $p$ and $q$ is true exactly in the following rows:

and:

The corresponding DNF is:

This formula is true exactly in those rows.

To construct a CNF formula, take each row in which the formula is false. For each such row, write a clause that excludes exactly that row. Then take the conjunction of all such clauses.

If the false rows are:

and:

then the corresponding clauses are:

and:

Thus the CNF is:

Lemma 1.33 (Truth Table Normal Forms)

Every truth table determines a DNF formula and a CNF formula with the same truth values as the table.

Proof

For DNF, each true row is represented by a term that is true exactly on that row. The disjunction of all such terms is true exactly when at least one true row is matched, and therefore it has the same truth table as the original formula.

For CNF, each false row is represented by a clause that is false exactly on that row. The conjunction of all such clauses is true exactly when none of the false rows is matched, and therefore it has the same truth table as the original formula.

Size of Normal Forms

Although every formula has an equivalent CNF and DNF, the converted formula may be much larger than the original one.

For example, repeated distribution can duplicate subformulas. A short formula may therefore produce a normal form whose size grows exponentially in the number of variables.

This matters in computation, because normal forms are useful for algorithms, but converting formulas naively can be inefficient for large inputs.

Connection with Computation

CNF is especially important in satisfiability solving, because many SAT solvers take formulas in conjunctive normal form as input.

A CNF formula represents a list of constraints:

To satisfy the formula, every clause $C_i$ must be true.

DNF has a different interpretation. A DNF formula represents a list of sufficient cases:

To satisfy the formula, it is enough for one term $T_i$ to be true.