The same logical formula can be written in infinitely many equivalent ways. To compare formulas, simplify them or feed them to a program, it helps to reduce them to a standard form. The two most widely used standard forms are disjunctive normal form (DNF) and conjunctive normal form (CNF). Understanding them also means understanding how automated verification tools and circuit designers work.
The building blocks: literals and clauses
- A literal is a variable or its negation: p, ¬p, q, ¬q.
- A conjunction of literals is an AND of literals, for example p ∧ ¬q ∧ r.
- A clause is an OR of literals, for example ¬p ∨ q ∨ ¬r.
With these blocks:
- DNF is an OR of conjunctions of literals: (p ∧ ¬q) ∨ (¬p ∧ r) ∨ q;
- CNF is an AND of clauses: (p ∨ q) ∧ (¬p ∨ r) ∧ (¬q ∨ ¬r).
One way to remember them: DNF describes the cases in which the formula is true ("it is true if this happens, or this, or this"); CNF lists constraints that must all hold together ("this must hold, and this, and this").
Deriving DNF from a truth table
The method is mechanical. For each row where the formula is T, write a conjunction that describes exactly that row: the variable as it is if it is T, negated if it is F. Then join them all with OR.
Take the formula "exactly one of p and q is true" (XOR):
| p | q | p ⊕ q |
|---|---|---|
| T | T | F |
| T | F | T |
| F | T | T |
| F | F | F |
The true rows are the second (p true, q false) and the third (p false, q true). The DNF is therefore (p ∧ ¬q) ∨ (¬p ∧ q).
Deriving CNF from a truth table
The method is the dual. For each row where the formula is F, write a clause that is false only in that row: the variable negated if it is T, as it is if it is F. Then join the clauses with AND.
For XOR the false rows are the first (p and q true) and the fourth (both false). The first gives the clause ¬p ∨ ¬q, the fourth p ∨ q. The CNF is (p ∨ q) ∧ (¬p ∨ ¬q). It reads nicely: "at least one is true, and not both are true".
Algebraic transformation
When the table is too large, you work with equivalences:
- Eliminate ↔ and →, using p → q ≡ ¬p ∨ q.
- Push negations down to the literals with De Morgan and double negation.
- Apply distributivity: for CNF, distribute ∨ over ∧; for DNF, ∧ over ∨.
Example: convert p ∨ (q ∧ r) to CNF. Distributing gives (p ∨ q) ∧ (p ∨ r).
There is a practical problem: distributivity can make the formula grow exponentially. The formula (a₁ ∧ b₁) ∨ (a₂ ∧ b₂) ∨ … ∨ (aₙ ∧ bₙ) has an equivalent CNF with 2ⁿ clauses. That is why real tools use the Tseitin transformation, which introduces auxiliary variables and produces a CNF of linear size. The result is not equivalent in the strict sense, but it is equisatisfiable: it is satisfiable if and only if the original is, and for many purposes that is enough.
Why CNF matters so much
The SAT problem asks whether a formula has at least one assignment that makes it true. The programs that solve it, SAT solvers, almost always accept input in CNF, often in the text format called DIMACS:
p cnf 3 2
1 -2 0
2 3 0
The header line says there are 3 variables and 2 clauses; each following line is a clause, with negative numbers for negated literals and zero as a terminator. This example represents (x₁ ∨ ¬x₂) ∧ (x₂ ∨ x₃).
CNF suits automated search because each clause is an independent constraint: if a partial assignment makes every literal of a clause false except one, that last literal is forced. This rule, called unit propagation, is at the heart of the DPLL and CDCL algorithms. SAT solvers are used to verify hardware, plan, solve combinatorial puzzles and analyse dependencies between software packages.
What about DNF?
DNF makes the opposite question trivial: a formula in DNF is satisfiable if at least one of its conjunctions does not contain a variable together with its negation. The price is that checking whether a DNF is a tautology becomes hard. In circuit design DNF corresponds to the "sum of products" structure, built with one level of AND gates followed by an OR gate, and it is minimised with Karnaugh maps or the Quine-McCluskey algorithm.
In short
- DNF is an OR of ANDs of literals; CNF is an AND of ORs of literals, that is, of clauses.
- From the truth table: true rows give the DNF, false rows give the CNF.
- Algebraic conversion can blow up exponentially; Tseitin produces an equisatisfiable CNF of linear size.
- SAT solvers work in CNF, typically in DIMACS format.
- DNF corresponds to "sum of products" circuits.
