CNF vs DNF: differences, examples and when to use each

Conjunctive normal form is an AND of OR-clauses; disjunctive normal form is an OR of AND-terms. For (A -> B) AND (B -> C) the CNF has two clauses and the DNF three terms, and the Karnaugh map finds a two-term cover the algebraic DNF missed.

The engine converts the formula both ways. Eliminating the two implications gives the CNF directly, (NOT A OR B) AND (NOT B OR C), two clauses with four literals: two constraints, each a chain link. The DNF needs distribution and a complement step on top, and comes out as (NOT A AND NOT B) OR (NOT A AND C) OR (B AND C), three terms. The function is TRUE on rows 0, 1, 3 and 7, Σm(0, 1, 3, 7).

The Karnaugh map derives (NOT A AND NOT B) OR (B AND C), two groups, while reporting three prime implicants: the middle term of the algebraic DNF, NOT A AND C, is the consensus of the other two and is covered by them. That is the difference between a conversion and a reduction. The converter produces a correct normal form by rewriting; the map looks for a cover; neither is wrong, and the exact check confirms both against the original.

The choice is by use. CNF is what a SAT solver reads, one clause per constraint, and what a specification of requirements naturally produces. DNF is what a rule reads like as cases, what a decision table's columns are, and what a Karnaugh map produces. The gate counts, eleven NAND and five NOR here, follow the structure rather than the form name.

Example

f := (A -> B) AND (B -> C) · output

Exact checks

Always true (tautology)? No Counterexample: A = F, B = T, C = F · Exhaustively checked and solver cross-checked · 3 rows

Always false (contradiction)? No Counterexample: A = F, B = F, C = F · Exhaustively checked and solver cross-checked · 1 rows

Can be true? Yes Example assignment: A = F, B = F, C = F · Exhaustively checked and solver cross-checked · 1 rows

Truth table (8 rows)

CNF vs DNF: differences, examples and when to use each
#	A	B	C	f
0	FALSE	FALSE	FALSE	TRUE
1	FALSE	FALSE	TRUE	TRUE
2	FALSE	TRUE	FALSE	FALSE
3	FALSE	TRUE	TRUE	TRUE
4	TRUE	FALSE	FALSE	FALSE
5	TRUE	FALSE	TRUE	FALSE
6	TRUE	TRUE	FALSE	FALSE
7	TRUE	TRUE	TRUE	TRUE

Logic diagram

Karnaugh map

A \ BC

1m0

1m1

1m3

0m2

0m4

0m5

1m7

0m6

cells m0, m1NOT A AND NOT B
cells m3, m7B AND C

(NOT A AND NOT B) OR (B AND C) · Derived (NOT A AND NOT B) OR (B AND C). Exactly equivalent on every assignment.

Minterms and maxterms

f(A, B, C) = Σm(0, 1, 3, 7)f(A, B, C) = ΠM(2, 4, 5, 6)

Variable order: A, B, C · 8 rows

Normal forms

Conjunctive normal form (CNF)

(NOT A OR B) AND (NOT B OR C)

2 clauses, 4 literals · complete · Implication elimination ×2

Disjunctive normal form (DNF)

(NOT A AND NOT B) OR (NOT A AND C) OR (B AND C)

3 terms, 6 literals · complete · Implication elimination ×2, Distribution ×1, Complement ×1

NAND-only and NOR-only

NAND-only form

NAND(NAND(NAND(A, NAND(B, B)), NAND(B, NAND(C, C))), NAND(NAND(A, NAND(B, B)), NAND(B, NAND(C, C))))

11 gates · verified equivalent on every row

NOR-only form

NOR(NOR(NOR(A, A), B), NOR(NOR(B, B), C))

5 gates · verified equivalent on every row

The common slip

Expecting the DNF to be the shortest OR-of-ANDs form. The converter's three-term DNF is a valid normal form with a consensus term the map removes; “normal form” promises a shape, not the absence of removable terms.

Questions

Can a formula have several DNFs?

Yes. The canonical DNF, one minterm per TRUE row, is unique; shorter DNFs are not, and (NOT A AND NOT B) OR (B AND C) and the three-term form are both DNFs of this function.

Why does CNF suit solvers?

Because a solver's core operation is checking clauses, each an OR of literals that must be satisfied, and unit propagation works clause by clause. The SMT-LIB export phrases its questions so that the solver's job is exactly this.

Practice

CNF and DNF exercises with answers

Compare

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.