Normal forms

Why a normal form

The same idea can be written in a thousand ways: $p \to q$, $\lnot p \lor q$, $\lnot q \to \lnot p$, $\lnot(p \land \lnot q)$ are equivalent. To compare two formulas, simplify them, or feed them to a program, we bring them to a normal form: a standard way of writing, built with $\lnot$, $\land$ and $\lor$ only, and in a prescribed order.

The two forms of this chapter are the ones tools use: conjunctive normal form is the input of SAT solvers (chapter 4) and of resolution (chapter 5).

Vocabulary

• A literal is a variable or its negation: $p$, $\lnot q$.
• A clause is a disjunction of literals: $p \lor \lnot q \lor r$. A single literal is a clause; the empty clause, with no literal, is $\bot$.
• A monomial is a conjunction of literals: $p \land \lnot q \land r$.

A formula is in:

• conjunctive normal form (CNF) if it is a conjunction of clauses: $(p \lor q) \land (\lnot p \lor r) \land \lnot q$;
• disjunctive normal form (DNF) if it is a disjunction of monomials: $(p \land q) \lor (\lnot p \land r) \lor \lnot q$.

Mnemonic: in a CNF, the main connective is conjunction.

Normal form by computation

Three steps

1. Eliminate $\leftrightarrow$ and $\to$: $A \leftrightarrow B \equiv (A \to B) \land (B \to A)$, then $A \to B \equiv \lnot A \lor B$.
2. Push the negations down to the variables, with De Morgan and double negation. We obtain the negation normal form: the $\lnot$ now apply only to variables.
3. Distribute:
4. for a CNF, $\lor$ over $\land$: $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$;
5. for a DNF, $\land$ over $\lor$: $A \land (B \lor C) \equiv (A \land B) \lor (A \land C)$.

We finish by simplifying: a clause containing $p$ and $\lnot p$ is $\top$ and disappears from a CNF; a monomial containing $p$ and $\lnot p$ is $\bot$ and disappears from a DNF; absorption removes a clause that contains another one.

Normal form from the truth table

Each row of the table is described by a monomial: the row $p = 1, q = 0$ is described by $p \land \lnot q$, true on that row and nowhere else.

• DNF: the disjunction of the monomials of the rows where the formula is 1.
• CNF: the conjunction of the negations of the rows where the formula is 0. The negation of the monomial $p \land \lnot q$ is the clause $\lnot p \lor q$.

This method proves that every formula has a DNF and a CNF: just read its table. It has one drawback: the table has $2^n$ rows.

What it costs

Distribution can make the size explode. The formula

is a DNF with $2n$ literals. Its CNF picks one literal in each parenthesis, in every possible way: it has $2^n$ clauses. For $n = 30$, more than a billion.

So we do not look for an equivalent CNF when it is too large: solvers use an equisatisfiable CNF (satisfiable if and only if the original formula is), obtained by adding new variables, which stays of linear size. This is the Tseitin transformation, not covered here.

What it proves: three connectives are enough

Since every formula has a DNF, every truth table can be written with $\lnot$, $\land$ and $\lor$ only. We say that $\{\lnot, \land, \lor\}$ is a functionally complete set.

We can go further down: $A \lor B \equiv \lnot(\lnot A \land \lnot B)$, so $\{\lnot, \land\}$ is enough. And a single connective is enough, “not-and” ($p \uparrow q$, true except when $p$ and $q$ both are): $\lnot p \equiv p \uparrow p$. This is why an electronic circuit can be built entirely out of NAND gates.

“Exactly one out of $n$”

A frequent constraint in modelling: exactly one of the propositions $p_1, \ldots, p_n$ is true. In CNF it is written as the conjunction of two constraints:

• at least one: the clause $p_1 \lor p_2 \lor \cdots \lor p_n$;
• at most one: for each pair, $\lnot p_i \lor \lnot p_j$.

For three propositions: $(p \lor q \lor r) \land (\lnot p \lor \lnot q) \land (\lnot p \lor \lnot r) \land (\lnot q \lor \lnot r)$.