Normal Forms: CNF and DNF

in progressThis lesson is still being built - content, demos, and checkpoints may change before release.

Normal forms

Loading interactive demo…

The table on the left is the formula's truth table, rows counted down from all true. The sheet on the right is the derivation: on the table route, one clause per false row (CNF) or one term per true row (DNF), then the form; on the rewrite route, the formula after every equivalence applied, indented by pass (arrows, then negations, then distribution), then the form.Take the tour, or press and explore. Legend:

The panel beside the stage is the real NormalFormConverter class from the published library executing in your browser, with the current line highlighted.

The row being read, or the line just written.
Rows already turned into a clause or a term.
The tapped line, and the row it came from.
The finished form, checked equivalent to the original.

clauses counts the clauses or terms so far, literals the literals they hold, lines the rows read or rewrites made, equivalent whether the result matches the original on every row. Tap a line on the sheet to light the row it came from.

The code panel shows bare executable code by default. The bar above it names the file (hover the name for the full published path); options holds the toggles: comments, the tracer instrumentation that produces this visualization, and verbose names for the terse identifiers (display only: the default is the byte-exact published file). The view switch adds plain-English narration: both interleaves it with the code, pseudo shows only the pseudocode. hide code collapses the panel; the rail it leaves behind brings it back.

Keys: Space play/pause · ←/→ step · Home/End jump · R reset · F fullscreen · G guided tour

Literals, clauses, terms. A literal is a variable or its negation. A clause is an or of literals; a term is an and of literals. A formula is in conjunctive normal form (CNF) when it is an and of clauses, and in disjunctive normal form (DNF) when it is an or of terms:

\text{CNF:}\; (p \vee \neg q) \wedge (\neg p \vee r), \qquad \text{DNF:}\; (p \wedge \neg q) \vee (\neg p \wedge r) .

Every formula has both forms, and the stage shows two ways to get there.

Reading the table. A row of the truth table is picked out by one term: each variable as it stands on that row. The or of the terms for the true rows is true exactly on those rows, so it is the formula: that is a DNF. Dually, a row is ruled out by one clause: each variable negated as it stands there, false on that row alone. The and of the clauses for the false rows is false exactly there, and that is a CNF. Both are correct by construction, and both can be large: a formula false on most of its $2^n$ rows gets nearly $2^n$ clauses of $n$ literals each.

Rewriting. The other route never looks at the table. Three passes of equivalences, each preserving the truth table, change the formula's shape:

p \to q \equiv \neg p \vee q, \qquad \neg (p \wedge q) \equiv \neg p \vee \neg q, \qquad p \vee (q \wedge r) \equiv (p \vee q) \wedge (p \vee r) .

First every arrow becomes not-and-or (an iff becomes two arrows); then negations are pushed down by De Morgan's laws, a double negation cancelling, until every $\neg$ sits on a variable; then or is distributed over and (for CNF) or and over or (for DNF). The result is often smaller than the table's, but distribution can double a part each time it fires: the blow-up preset, an or of two-literal terms, gets $2^n$ clauses from $n$ terms.

Why CNF. A clause is easy to check: it holds unless every literal in it is false. That makes CNF the input of choice for the SAT solver in the next lesson, whose whole search is about assigning variables so that no clause is left with all its literals false, and for resolution, whose single rule works on two clauses at a time. Solvers avoid the blow-up by Tseitin's transformation: name each subformula with a fresh variable and add short clauses tying the name to its parts, which keeps the size linear at the cost of extra variables.

That any Boolean formula can be written as a sum of products goes back to Boole's algebra, and the systematic use of the two normal forms as a proof tool is in Hilbert and Ackermann's 1928 textbook, which proved the propositional calculus complete by reducing every formula to one. Quine and McCluskey gave the method for the smallest sum of products in the 1950s, and Karnaugh the map for doing it by eye; for solvers it was Grigori Tseitin's 1968 observation that a formula can be put into clauses with only linear growth, by naming its parts, that made conjunctive normal form the common input.

1928David Hilbert and Wilhelm Ackermann - 'Principles of Mathematical Logic' uses conjunctive normal form to prove the propositional calculus complete and decidable.source
1952Willard Van Orman Quine - Describes the prime implicant method for the smallest disjunctive normal form, which McCluskey turns into a tabular algorithm in 1956.source
1953Maurice Karnaugh - Publishes the map that lets an engineer read a minimal sum of products off a truth table by circling blocks of ones.source
1960Martin Davis and Hilary Putnam - Their satisfiability procedure takes clauses as input, fixing conjunctive normal form as the shape solvers want.source
1968Grigori Tseitin - Shows that introducing a fresh variable for each subformula gives an equisatisfiable CNF of linear size, avoiding the exponential blow-up of distribution.source

Used today

SAT solvers - Every industrial solver reads clauses; a circuit or a program is translated to CNF, by Tseitin's method, before it is checked.
Circuit design - A sum of products is a two-level circuit of and gates feeding an or; minimising it is minimising the chip.
Database queries - Query planners rewrite a where clause into normal form so that each conjunct can be matched to an index.

formula

route

form

clauses: 2
literals: 4
lines: 2
equivalent: yes

normal-forms.ts

import type { Tracer } from "../trace";import { clausesOf, dedupe, isTautologous, normalFormText, type Clause, type NormalForm, type NormalFormKind } from "./clauses";import { FormulaPrinter, assignments, evaluate, variables, type Formula } from "./formula";export type RewriteRule = "eliminate-implication" | "push-negation" | "distribute";export interface RewriteStep {  rule: RewriteRule;  /** The subformula rewritten and what it became. */  before: string;  after: string;  /** The whole formula after the step. */  formula: string;}export interface NormalFormReport {  form: NormalForm;  text: string;  /** The rewrite route's steps; empty on the table route. */  steps: RewriteStep[];}/** The most rewrite steps a formula may take before the converter gives up: distribution can blow up. */export const MAX_REWRITES = 64;/** * Two ways to the normal forms. The table route reads the form off the * truth table: a disjunctive normal form is one term per true row, * the literals that pick that row out; a conjunctive normal form is * one clause per false row, the literals that rule that row out. The * rewrite route transforms the formula itself by equivalences, one * node at a time: arrows become ors, negations are pushed down to the * variables by De Morgan's laws, and then or is distributed over and * (for CNF) or and over or (for DNF) until the shape is right. Both * routes give an equivalent formula; the table route's can be larger, * the rewrite route's can blow up exponentially on the distribution. * * Time: O(2^n) for the table route; up to exponential for the rewrite route. Space: the same. */export class NormalFormConverter {  constructor(private readonly tracer?: Tracer) {}  /** The form read off the truth table, row by row. */  fromTable(formula: Formula, kind: NormalFormKind): NormalFormReport {    const names = variables(formula);    const clauses: Clause[] = [];    assignments(names).forEach((values, row) => {      const value = evaluate(formula, values);      if (kind === "dnf" && value) {        // The term true on exactly this row: each variable as it stands here.        const term: Clause = names.map((name) => ({ name, negated: !values.get(name) }));        clauses.push(term);        // ▸ a true row becomes a term: every variable as it stands on that row        this.tracer?.emit("read-true-row", { row, values: Object.fromEntries(values), clause: term.map((l) => ({ ...l })), count: clauses.length });      }      if (kind === "cnf" && !value) {        // The clause false on exactly this row: each variable negated as it stands here.        const clause: Clause = names.map((name) => ({ name, negated: values.get(name) ?? false }));        clauses.push(clause);        // ▸ a false row becomes a clause: every variable negated as it stands on that row        this.tracer?.emit("read-false-row", { row, values: Object.fromEntries(values), clause: clause.map((l) => ({ ...l })), count: clauses.length });      }    });    return { ...this.assemble(kind, clauses, "table"), steps: [] };  }  /** The form reached by rewriting the formula with equivalences, one node at a time. */  rewrite(formula: Formula, kind: NormalFormKind): NormalFormReport {    let current = formula;    let formulaSoFar = formula;    const steps: RewriteStep[] = [];    const rules: RewriteRule[] = ["eliminate-implication", "push-negation", "distribute"];    for (const rule of rules) {      for (;;) {        if (steps.length >= MAX_REWRITES) throw new RangeError(`more than ${MAX_REWRITES} rewrites: the form blows up`);        const hit = NormalFormConverter.apply(current, rule, kind);        const matchedNode = NormalFormConverter.apply(formulaSoFar, rule, kind);        if (!hit) break;        if (!matchedNode) break;        current = hit.formula;        formulaSoFar = matchedNode.formula;        const step: RewriteStep = { rule, before: FormulaPrinter.print(hit.before), after: FormulaPrinter.print(hit.after), formula: FormulaPrinter.print(current) };        const step: RewriteStep = { rule, before: FormulaPrinter.print(matchedNode.before), after: FormulaPrinter.print(matchedNode.after), formula: FormulaPrinter.print(formulaSoFar) };        steps.push(step);        const payload = { before: step.before, after: step.after, formula: step.formula, step: steps.length };        // ▸ an arrow is a not and an or; an iff is two arrows        if (rule === "eliminate-implication") this.tracer?.emit("eliminate-implication", payload);        // ▸ a not over a not vanishes; over an and or an or it flips the connective and sinks        else if (rule === "push-negation") this.tracer?.emit("push-negation", payload);        // ▸ or over and gives two ors (for CNF); and over or gives two ands (for DNF)        else this.tracer?.emit("distribute", payload);      }    }    const clauses = clausesOf(current, kind).map(dedupe).filter((clause) => !isTautologous(clause));    const clauses = clausesOf(formulaSoFar, kind).map(dedupe).filter((clause) => !isTautologous(clause));    return { ...this.assemble(kind, clauses, "rewrite"), steps };  }  /** The clauses joined into the form, printed once for both routes. */  private assemble(kind: NormalFormKind, clauses: Clause[], route: "table" | "rewrite"): { form: NormalForm; text: string } {    const form: NormalForm = { kind, clauses };    const text = normalFormText(form);    // ▸ the clauses joined: ands of ors for CNF, ors of ands for DNF    this.tracer?.emit("assemble", { kind, clauses: clauses.length, text, route });    return { form, text };  }  /** The first node (outermost, left first) the rule applies to, rewritten; null when the rule has nothing left to do. */  private static apply(formula: Formula, rule: RewriteRule, kind: NormalFormKind): { formula: Formula; before: Formula; after: Formula } | null {    const after = NormalFormConverter.rewriteNode(formula, rule, kind);    if (after) return { formula: after, before: formula, after };    if (formula.kind === "var") return null;    if (formula.kind === "not") {      const inner = NormalFormConverter.apply(formula.operand, rule, kind);      return inner ? { formula: { kind: "not", operand: inner.formula }, before: inner.before, after: inner.after } : null;    }    const left = NormalFormConverter.apply(formula.left, rule, kind);    if (left) return { formula: { kind: formula.kind, left: left.formula, right: formula.right }, before: left.before, after: left.after };    const right = NormalFormConverter.apply(formula.right, rule, kind);    if (right) return { formula: { kind: formula.kind, left: formula.left, right: right.formula }, before: right.before, after: right.after };    return null;  }  /** The rule applied at this node alone, or null when it does not match here. */  private static rewriteNode(f: Formula, rule: RewriteRule, kind: NormalFormKind): Formula | null {    if (rule === "eliminate-implication") {      if (f.kind === "implies") return { kind: "or", left: { kind: "not", operand: f.left }, right: f.right };      if (f.kind === "iff") return { kind: "and", left: { kind: "or", left: { kind: "not", operand: f.left }, right: f.right }, right: { kind: "or", left: { kind: "not", operand: f.right }, right: f.left } };      return null;    }    if (rule === "push-negation") {      if (f.kind !== "not") return null;      const inner = f.operand;      if (inner.kind === "not") return inner.operand;      if (inner.kind === "and") return { kind: "or", left: { kind: "not", operand: inner.left }, right: { kind: "not", operand: inner.right } };      if (inner.kind === "or") return { kind: "and", left: { kind: "not", operand: inner.left }, right: { kind: "not", operand: inner.right } };      return null;    }    // Distribute: for CNF, or over and; for DNF, and over or.    const outer = kind === "cnf" ? "or" : "and";    const inner = kind === "cnf" ? "and" : "or";    if (f.kind !== outer) return null;    if (f.right.kind === inner) return { kind: inner, left: { kind: outer, left: f.left, right: f.right.left }, right: { kind: outer, left: f.left, right: f.right.right } };    if (f.left.kind === inner) return { kind: inner, left: { kind: outer, left: f.left.left, right: f.right }, right: { kind: outer, left: f.left.right, right: f.right } };    return null;  }}

clauses =: 2
form =: (not p or not q) and (p or q)
literals =: 4
equivalent =: yes

(not p or not q) and (p or q): 2 clauses, 4 literals; equivalent to the original on every row.

import type { Tracer } from "../trace";import { clausesOf, dedupe, isTautologous, normalFormText, type Clause, type NormalForm, type NormalFormKind } from "./clauses";import { FormulaPrinter, assignments, evaluate, variables, type Formula } from "./formula";export type RewriteRule = "eliminate-implication" | "push-negation" | "distribute";export interface RewriteStep { rule: RewriteRule; /** The subformula rewritten and what it became. */ before: string; after: string; /** The whole formula after the step. */ formula: string;}export interface NormalFormReport { form: NormalForm; text: string; /** The rewrite route's steps; empty on the table route. */ steps: RewriteStep[];}/** The most rewrite steps a formula may take before the converter gives up: distribution can blow up. */export const MAX_REWRITES = 64;/** * Two ways to the normal forms. The table route reads the form off the * truth table: a disjunctive normal form is one term per true row, * the literals that pick that row out; a conjunctive normal form is * one clause per false row, the literals that rule that row out. The * rewrite route transforms the formula itself by equivalences, one * node at a time: arrows become ors, negations are pushed down to the * variables by De Morgan's laws, and then or is distributed over and * (for CNF) or and over or (for DNF) until the shape is right. Both * routes give an equivalent formula; the table route's can be larger, * the rewrite route's can blow up exponentially on the distribution. * * Time: O(2^n) for the table route; up to exponential for the rewrite route. Space: the same. */export class NormalFormConverter { constructor(private readonly tracer?: Tracer) {} /** The form read off the truth table, row by row. */ fromTable(formula: Formula, kind: NormalFormKind): NormalFormReport { const names = variables(formula); const clauses: Clause[] = []; assignments(names).forEach((values, row) => { const value = evaluate(formula, values); if (kind === "dnf" && value) { // The term true on exactly this row: each variable as it stands here. const term: Clause = names.map((name) => ({ name, negated: !values.get(name) })); clauses.push(term); // ▸ a true row becomes a term: every variable as it stands on that row this.tracer?.emit("read-true-row", { row, values: Object.fromEntries(values), clause: term.map((l) => ({ ...l })), count: clauses.length }); } if (kind === "cnf" && !value) { // The clause false on exactly this row: each variable negated as it stands here. const clause: Clause = names.map((name) => ({ name, negated: values.get(name) ?? false })); clauses.push(clause); // ▸ a false row becomes a clause: every variable negated as it stands on that row this.tracer?.emit("read-false-row", { row, values: Object.fromEntries(values), clause: clause.map((l) => ({ ...l })), count: clauses.length }); } }); return { ...this.assemble(kind, clauses, "table"), steps: [] }; } /** The form reached by rewriting the formula with equivalences, one node at a time. */ rewrite(formula: Formula, kind: NormalFormKind): NormalFormReport { let current = formula; let formulaSoFar = formula; const steps: RewriteStep[] = []; const rules: RewriteRule[] = ["eliminate-implication", "push-negation", "distribute"]; for (const rule of rules) { for (;;) { if (steps.length >= MAX_REWRITES) throw new RangeError(`more than ${MAX_REWRITES} rewrites: the form blows up`); const hit = NormalFormConverter.apply(current, rule, kind); const matchedNode = NormalFormConverter.apply(formulaSoFar, rule, kind); if (!hit) break; if (!matchedNode) break; current = hit.formula; formulaSoFar = matchedNode.formula; const step: RewriteStep = { rule, before: FormulaPrinter.print(hit.before), after: FormulaPrinter.print(hit.after), formula: FormulaPrinter.print(current) }; const step: RewriteStep = { rule, before: FormulaPrinter.print(matchedNode.before), after: FormulaPrinter.print(matchedNode.after), formula: FormulaPrinter.print(formulaSoFar) }; steps.push(step); const payload = { before: step.before, after: step.after, formula: step.formula, step: steps.length }; // ▸ an arrow is a not and an or; an iff is two arrows if (rule === "eliminate-implication") this.tracer?.emit("eliminate-implication", payload); // ▸ a not over a not vanishes; over an and or an or it flips the connective and sinks else if (rule === "push-negation") this.tracer?.emit("push-negation", payload); // ▸ or over and gives two ors (for CNF); and over or gives two ands (for DNF) else this.tracer?.emit("distribute", payload); } } const clauses = clausesOf(current, kind).map(dedupe).filter((clause) => !isTautologous(clause)); const clauses = clausesOf(formulaSoFar, kind).map(dedupe).filter((clause) => !isTautologous(clause)); return { ...this.assemble(kind, clauses, "rewrite"), steps }; } /** The clauses joined into the form, printed once for both routes. */ private assemble(kind: NormalFormKind, clauses: Clause[], route: "table" | "rewrite"): { form: NormalForm; text: string } { const form: NormalForm = { kind, clauses }; const text = normalFormText(form); // ▸ the clauses joined: ands of ors for CNF, ors of ands for DNF this.tracer?.emit("assemble", { kind, clauses: clauses.length, text, route }); return { form, text }; } /** The first node (outermost, left first) the rule applies to, rewritten; null when the rule has nothing left to do. */ private static apply(formula: Formula, rule: RewriteRule, kind: NormalFormKind): { formula: Formula; before: Formula; after: Formula } | null { const after = NormalFormConverter.rewriteNode(formula, rule, kind); if (after) return { formula: after, before: formula, after }; if (formula.kind === "var") return null; if (formula.kind === "not") { const inner = NormalFormConverter.apply(formula.operand, rule, kind); return inner ? { formula: { kind: "not", operand: inner.formula }, before: inner.before, after: inner.after } : null; } const left = NormalFormConverter.apply(formula.left, rule, kind); if (left) return { formula: { kind: formula.kind, left: left.formula, right: formula.right }, before: left.before, after: left.after }; const right = NormalFormConverter.apply(formula.right, rule, kind); if (right) return { formula: { kind: formula.kind, left: formula.left, right: right.formula }, before: right.before, after: right.after }; return null; } /** The rule applied at this node alone, or null when it does not match here. */ private static rewriteNode(f: Formula, rule: RewriteRule, kind: NormalFormKind): Formula | null { if (rule === "eliminate-implication") { if (f.kind === "implies") return { kind: "or", left: { kind: "not", operand: f.left }, right: f.right }; if (f.kind === "iff") return { kind: "and", left: { kind: "or", left: { kind: "not", operand: f.left }, right: f.right }, right: { kind: "or", left: { kind: "not", operand: f.right }, right: f.left } }; return null; } if (rule === "push-negation") { if (f.kind !== "not") return null; const inner = f.operand; if (inner.kind === "not") return inner.operand; if (inner.kind === "and") return { kind: "or", left: { kind: "not", operand: inner.left }, right: { kind: "not", operand: inner.right } }; if (inner.kind === "or") return { kind: "and", left: { kind: "not", operand: inner.left }, right: { kind: "not", operand: inner.right } }; return null; } // Distribute: for CNF, or over and; for DNF, and over or. const outer = kind === "cnf" ? "or" : "and"; const inner = kind === "cnf" ? "and" : "or"; if (f.kind !== outer) return null; if (f.right.kind === inner) return { kind: inner, left: { kind: outer, left: f.left, right: f.right.left }, right: { kind: outer, left: f.left, right: f.right.right } }; if (f.left.kind === inner) return { kind: inner, left: { kind: outer, left: f.left.left, right: f.right }, right: { kind: outer, left: f.left.right, right: f.right } }; return null; }}