Conjunctive Normal Form

Introduction to CNF

Conjunctive Normal Form (CNF) is a standard way to write Boolean expressions:

CNF = AND of ORs (product of sums)

Structure: (claus$e_1$) $\land$ (claus$e_2$) $\land$ ... $\land$ (clauseₙ)

Where each clause is an OR of literals (variables or their complements).

Examples:

• (A $\lor$ B) $\land$ ($\neg$A $\lor$ C) - CNF with 2 clauses
• A $\lor$ B $\lor$ C - CNF with 1 clause
• (P $\lor$ $\neg$Q) $\land$ ($\neg$P $\lor$ Q) $\land$ (P $\lor$ Q) - CNF with 3 clauses

Recognizing CNF

To check if an expression is in CNF:

1. Top level must be AND (or a single clause)
2. Each clause must be OR of literals only
3. No nested operations - no AND inside OR, no OR inside AND

Valid CNF:

• (A $\lor$ B) $\land$ (C $\lor$ D) ✓
• A $\lor$ B ✓ (single clause)
• A $\land$ B $\land$ C ✓ (each clause is one literal)

Not CNF:

• A $\lor$ (B $\land$ C) ✗ (AND nested inside OR)
• (A $\land$ B) $\lor$ (C $\land$ D) ✗ (OR at top level with AND terms)

CNF from Truth Table

To write a function in CNF from its truth table:

1. Find all rows where output is FALSE (0)
2. Write the maxterm for each FALSE row
3. AND all maxterms together

Example for f(A,B) = 0 when A=0,B=0 or A=1,B=0:

• Row A=0,B=0 $\to$ maxterm: A $\lor$ B
• Row A=1,B=0 $\to$ maxterm: $\neg$A $\lor$ B
• CNF: (A $\lor$ B) $\land$ ($\neg$A $\lor$ B)

This is called the canonical CNF or product of maxterms.

Product of Maxterms Notation

The product of maxterms notation uses $\Pi$ (pi) to list which maxterms are ANDed:

f(A,B) = $\Pi$M(0, 2) means: f = $M_0$ $\land$ $M_2$

Where $M_0$ = A $\lor$ B and $M_2$ = $\neg$A $\lor$ B.

This is shorthand for listing all the truth table rows where f is FALSE.

Examples (for variables A, B):

• $\Pi$M(3) = $\neg$A $\lor$ $\neg$B (false only at row 3)
• $\Pi$M(1, 2) = (A $\lor$ $\neg$B) $\land$ ($\neg$A $\lor$ B)
• $\Pi$M() = 1 (no false rows = always true)

Canonical CNF

Canonical CNF (also called "full CNF" or "complete product of maxterms"):

• Every clause is a full maxterm (includes ALL variables)
• Each maxterm appears exactly once
• Unique representation for each function

Non-canonical CNF:

• Clauses may not include all variables
• May be simplified but still valid CNF

Example for f(A,B) = A:

• Canonical: (A $\lor$ B) $\land$ (A $\lor$ $\neg$B)
• Simplified: A (single-literal clause is valid CNF)

Evaluating CNF Expressions

To evaluate a CNF expression:

1. Evaluate each OR clause separately
2. AND the results together

Since CNF is AND of ORs:

• The expression is FALSE if any one clause is FALSE
• Each clause is FALSE only if all its literals are FALSE

Example: (A $\lor$ $\neg$B) $\land$ ($\neg$A $\lor$ B) with A=1, B=1:

• First clause: 1 $\lor$ 0 = 1 ✓
• Second clause: 0 $\lor$ 1 = 1 ✓
• Both TRUE, so result is TRUE

Converting Expressions to CNF

To convert an expression to CNF:

Method 1: Truth Table

1. Build the truth table
2. Write maxterm for each FALSE row
3. AND all maxterms

Method 2: Algebraic

1. Eliminate implications/equivalences
2. Move NOTs inward (De Morgan's)
3. Distribute OR over AND

Example: A $\lor$ (B $\land$ C)

• Distribute: (A $\lor$ B) $\land$ (A $\lor$ C) $\leftarrow$ CNF!

Properties of CNF

Key CNF Properties:

1. Universality: Any Boolean function can be written in CNF
2. Canonical uniqueness: The canonical CNF (product of maxterms) is unique
3. Easy FALSE detection: Expression is FALSE if ANY clause is FALSE
4. Unit propagation: If a clause has one literal, that literal must be true

Applications:

• SAT solvers (most use CNF as input format)
• Automated theorem proving
• Hardware verification

Comparing DNF and CNF

DNF and CNF are duals of each other:

CNF from Natural Language

Natural language to CNF:

When specs list requirements as "this AND that AND the other," where each requirement allows alternatives, you're looking at CNF:

• Each requirement becomes a clause (OR of options)
• Requirements combined with AND
• Result: (Optio$n_1$ $\lor$ Optio$n_2$) $\land$ (Optio$n_3$ $\lor$ Optio$n_4$) $\land$ ...

CNF matches how we express constraints that must all be satisfied.

CNF and SAT Solvers

SAT (Satisfiability) solvers determine if a Boolean formula can be made true.

Why CNF?

• Standard input format for all modern SAT solvers
• Efficient algorithms exist for CNF (DPLL, CDCL)
• Easy to add new constraints (just AND another clause)
• Unit propagation works naturally

SAT solvers are used in verification, planning, cryptography, and more!

CNF Minimization

Minimizing CNF uses similar techniques to DNF:

• Resolution: (A $\lor$ B) $\land$ ($\neg$A $\lor$ C) can derive (B $\lor$ C)
• Subsumption: (A $\lor$ B) $\land$ (A $\lor$ B $\lor$ C) $\to$ keep only (A $\lor$ B)
• Absorption: Remove redundant clauses
• Unit propagation: Single-literal clauses fix values

Goal: Fewer and shorter clauses.

Complex Expression to CNF

Converting to CNF:

1. Eliminate implications: P $\to$ Q becomes $\neg$P $\lor$ Q
2. Push negations inward (De Morgan)
3. Distribute OR over AND: A $\lor$ (B $\land$ C) = (A $\lor$ B) $\land$ (A $\lor$ C)

Or: Build truth table, then write product of maxterms.

CNF as Constraints

Reading CNF semantically:

• Each clause = one constraint that must be satisfied
• The AND connecting them = "all of these must hold"
• Example: (A $\lor$ B) $\land$ ($\neg$A $\lor$ C) means "at least one of A, B must be true AND at least one of $\neg$A, C must be true"

Why this matters:

• Adding a new requirement = AND another clause (stays in CNF!)
• A single violated clause makes the whole formula false
• SAT solvers and constraint systems use CNF for this reason