Normal forms

The same idea can be said in many ways. A normal form is one fixed shape that every formula can be rewritten into, without changing its meaning. This guide covers the two most useful shapes, CNF and DNF, and how the app reaches them one step at a time. Each step swaps a part of the formula for an equivalent one, as defined in the basics guide.

Literals, clauses and terms

Normal forms are built from three kinds of pieces:

• A literal is a sentence letter or a negated sentence letter: P and ¬Q are literals, but ¬¬P and ¬(P ∧ Q) are not.
• A clause is one or more literals joined by ∨, such as P ∨ ¬Q ∨ R. It is true when at least one of its literals is.
• A term is one or more literals joined by ∧, such as P ∧ ¬Q. It is true only when all of its literals are.

A single literal counts both as a clause and as a term.

CNF and DNF

A formula is in conjunctive normal form (CNF) if it is one or more clauses joined by ∧: an AND of ORs, such as (P ∨ Q) ∧ (¬P ∨ R). It is in disjunctive normal form (DNF) if it is one or more terms joined by ∨: an OR of ANDs, such as (P ∧ R) ∨ (Q ∧ ¬P).

So a formula in either form uses only ∧, ∨ and ¬, and every ¬ sits directly on a letter. Some formulas are in both forms at once: ¬P ∨ Q is a single clause, so it is in CNF, and a disjunction of two one-letter terms, so it is in DNF too. P → Q and ¬(P ∧ Q) are in neither.

Why they matter

A CNF is a list of requirements: the formula is true exactly when every clause is. That is why most SAT solvers, programs that decide whether a formula can be made true, take their input in CNF. Hardware designs, timetables and puzzles are often written as large sets of clauses and handed to such a solver.

A DNF is a list of ways to be true: the formula is true exactly when some term is. So you can read valuations that make it true straight off it. In (P ∧ ¬Q) ∨ (P ∧ ¬R), the first term says that P true and Q false is enough, whatever R is.

Each form also makes one question easy. A DNF can be made true exactly when some term contains no letter together with its negation. A CNF is a tautology exactly when every clause contains some letter together with its negation. (Both tests assume that the literals are letters and negated letters. The app also counts ⊥ and ¬⊥ as literals: a term that contains ⊥ is never true, and a clause that contains ¬⊥ is always true.)

Worked example: a CNF

Take ¬(P → (Q ∧ R)): “it is not the case that if it rains, it is cold and windy”. The app rewrites a formula in a fixed order of passes. Each pass applies one kind of equivalence everywhere it can, and the app moves on only when the pass has nothing left to change.

The app prints this formula as ¬(P → Q ∧ R). Since ∧ binds more tightly than →, the brackets around Q ∧ R are not needed, and the steps below are written the way the app writes them.

1. Eliminate ↔. There is no ↔, so this pass changes nothing, and the app shows no step for it.
2. Eliminate →. A → B becomes ¬A ∨ B. Here A is P and B is Q ∧ R, which gives ¬(¬P ∨ Q ∧ R), that is, ¬(¬P ∨ (Q ∧ R)).
3. Push ¬ inward (De Morgan and Double negation). A ¬ stands in front of a disjunction. De Morgan’s law turns ¬(A ∨ B) into ¬A ∧ ¬B, giving ¬¬P ∧ ¬(Q ∧ R). That leaves a negated conjunction, and the other law turns ¬(A ∧ B) into ¬A ∨ ¬B: ¬¬P ∧ (¬Q ∨ ¬R). The app does both in one De Morgan step. Then double negation turns ¬¬P into P: P ∧ (¬Q ∨ ¬R). The app repeats these two kinds of step until every ¬ sits on a letter.
4. Fold constants. This pass only removes ⊥ and ¬⊥. There are none, so nothing changes.
5. Distribute. In a CNF, no ∨ may have a ∧ inside it. The only ∨ here joins ¬Q and ¬R, which are literals, so there is nothing to distribute.
6. Simplify. No clause repeats a literal or holds a letter together with its negation, so nothing changes.

The result, P ∧ (¬Q ∨ ¬R), has two clauses: P and ¬Q ∨ ¬R. It says that it rains, and that it is not both cold and windy. That is exactly when the conditional is false.

The same formula in DNF

Choose DNF as the target form, and the first passes run as before, up to P ∧ (¬Q ∨ ¬R). That is not yet a DNF, because the ∧ has a ∨ inside it. For a DNF, ∧ is distributed over ∨: A ∧ (B ∨ C) becomes (A ∧ B) ∨ (A ∧ C). That gives (P ∧ ¬Q) ∨ (P ∧ ¬R), which the app prints without brackets as P ∧ ¬Q ∨ P ∧ ¬R. Simplifying changes nothing.

Read the two terms as two ways for the formula to be true: it rains and it is not cold, or it rains and it is not windy.

Solve and Practice

Under the formula, choose the target form, CNF or DNF. The toolbar switches between two modes.

In Solve, the default, the app lists its rewriting steps as in the figures above. Each step shows the rule’s name, a one-line description, and the formula before and after it, with the changed parts picked out. The result comes last. If there is nothing to rewrite, the app says the formula is already in the target form.

In Practice, you write each line yourself. Type a formula equivalent to the line above and press Check step. The app compares the two lines by truth table and adds yours only if they are equivalent. You may take bigger or smaller steps than Solve does: any equivalent formula is accepted. Once your last line is in the target form, you are done. Hint names the next rewrite the app would make, and Remove last step and Start over let you back out.

Common mistakes

• Distributing the wrong way. For a CNF, distribute ∨ over ∧: A ∨ (B ∧ C) becomes (A ∨ B) ∧ (A ∨ C). For a DNF, it is the other way round. The wrong move still gives an equivalent formula, but it leads away from the form you want: P ∧ (¬Q ∨ ¬R) is already a CNF, and distributing ∧ over ∨ turns it into the DNF.
• Copying the outside part only once. When you distribute, the outside part goes into both new pieces: P ∨ (Q ∧ R) becomes (P ∨ Q) ∧ (P ∨ R), not (P ∨ Q) ∧ R.
• Dropping brackets that matter. Without its brackets, P ∧ (¬Q ∨ ¬R) becomes P ∧ ¬Q ∨ ¬R, which means (P ∧ ¬Q) ∨ ¬R: a different formula. The app leaves out only the brackets that the order of strength makes unnecessary.
• Pushing ¬ through without swapping. ¬(Q ∧ R) is ¬Q ∨ ¬R, not ¬Q ∧ ¬R: De Morgan’s laws swap ∧ and ∨. Likewise, ¬(P → Q) is not ¬P → ¬Q. Remove the → first.

The equivalences behind each step

Every step replaces a part of the formula with an equivalent part, so the whole formula stays equivalent too. The table lists the equivalences the app uses, with the name of the step that uses each.

The language has no symbol for “true”, so the app uses ¬⊥ instead, and counts ⊥ and ¬⊥ as literals. The Simplify step treats a clause (or a term) as a set of literals, which is why their order and grouping never matter.

Every formula has both forms

The passes show why. After the first two, no → or ↔ is left. Pushing ¬ inward ends with every ¬ on a letter or on ⊥. Distributing then moves every ∧ outside every ∨ (for CNF), or the other way round (for DNF). Each pass finishes, and each step keeps the formula equivalent, so the end result is an equivalent CNF or DNF.

Normal forms are not unique. The rows of the truth table where ¬(P → (Q ∧ R)) is true give the longer DNF (P ∧ Q ∧ ¬R) ∨ (P ∧ ¬Q ∧ R) ∨ (P ∧ ¬Q ∧ ¬R), which is equivalent to the app’s P ∧ ¬Q ∨ P ∧ ¬R.

Reading the forms off a truth table

A truth table gives both forms directly. Take P ↔ Q:

• DNF from the true rows. Describe each row where the formula is true by a term: row 1 (P and Q true) by P ∧ Q, and row 4 (both false) by ¬P ∧ ¬Q. Joined by ∨, they give (P ∧ Q) ∨ (¬P ∧ ¬Q), which is true in exactly those rows.
• CNF from the false rows. For each row where the formula is false, write the clause that is false in that row and no other: row 2 (P true, Q false) gives ¬P ∨ Q, and row 3 gives P ∨ ¬Q. Joined by ∧, they give (¬P ∨ Q) ∧ (P ∨ ¬Q), which is false in exactly those rows.

Here both match what the app gives. This works for any formula, so it is a second proof that both forms always exist. If no row is true, use P ∧ ¬P as the DNF; if no row is false, use P ∨ ¬P as the CNF. The same construction shows that the connectives are truth-functionally complete.

The cost: exponential blow-up

Distribution copies: in A ∨ (B ∧ C) becoming (A ∨ B) ∧ (A ∨ C), A is written twice. Repeated, the copies multiply. The formula (P ∧ Q) ∨ (R ∧ S) ∨ (T ∧ U) is already a DNF, so the app has nothing to do for DNF. Its CNF, though, needs one clause for each way of picking one letter from each pair, such as P ∨ R ∨ T: 2 × 2 × 2 = 8 clauses.

With n pairs, the CNF has 2ⁿ clauses, and no equivalent CNF has fewer. With 8 pairs, (P₁ ∧ Q₁) ∨ … ∨ (P₈ ∧ Q₈), the app’s CNF already has 256 clauses. With 9, some step would produce a formula of more than 5,000 symbols (counting letters, ⊥ and connectives, not brackets), so the app stops and says the formula is too big to rewrite step by step.

Avoiding the blow-up

A SAT solver does not need an equivalent CNF. It needs one that is equisatisfiable with the original: one that can be made true exactly when the original can. The Tseitin transformation builds such a CNF. It gives every compound part of the formula a new sentence letter of its own, and writes clauses that say each new letter has the same value as its part. Then it adds one more clause: the new letter for the whole formula, on its own, which says that the whole formula is true. Without that last clause, the other clauses could always be made true, even for a formula that can never be true.

Each part needs only a few clauses, so the result grows in proportion to the length of the formula, not exponentially. Any valuation that makes the original true can be turned into one that makes the CNF true, by giving each new letter the value of its part; and any valuation that makes the CNF true makes the original true. But the CNF is not equivalent to the original: a valuation can make the original true and give a new letter the wrong value, and then the CNF is false. The app does not do this: it shows only equivalent rewrites.

Further reading

The transformation is G. S. Tseitin’s, from his 1968 paper “On the complexity of derivation in propositional calculus”. For the semantic ideas behind every step here, such as equivalence, see the part on truth tables in forall x: Calgary, the free textbook whose proof rules the app uses. Its Metatheory part (Part IX) has a chapter on normal forms, which builds a DNF from the true rows of a truth table and a CNF from the false rows, as above, and a chapter on functional completeness. The truth tables guide shows how the app checks that two formulas are equivalent.