Mathwords logoMathwords

Conjunctive Normal Form — Definition, Formula & Examples

Conjunctive Normal Form (CNF) is a way of writing a logical formula as an AND of clauses, where each clause is an OR of literals (variables or their negations). Any propositional logic formula can be rewritten in CNF.

A propositional formula is in conjunctive normal form if it is a conjunction (AND) of one or more clauses, where each clause is a disjunction (OR) of one or more literals. A literal is either a propositional variable pp or its negation ¬p\neg p. Formally, a CNF formula has the structure (l1,1l1,k1)(l2,1l2,k2)(ln,1ln,kn)(l_{1,1} \lor \cdots \lor l_{1,k_1}) \land (l_{2,1} \lor \cdots \lor l_{2,k_2}) \land \cdots \land (l_{n,1} \lor \cdots \lor l_{n,k_n}), where each li,jl_{i,j} is a literal.

How It Works

To convert a formula to CNF, first eliminate conditionals and biconditionals using equivalences like pq¬pqp \to q \equiv \neg p \lor q. Next, push negations inward using De Morgan's laws so that ¬\neg applies only to individual variables. Finally, distribute \lor over \land to achieve the required structure. The result is a conjunction of disjunctive clauses, each containing only literals.

Worked Example

Problem: Convert the formula ¬(pq)r\neg(p \land q) \lor r into conjunctive normal form.
Step 1: Apply De Morgan's law to the negated conjunction.
¬(pq)r(¬p¬q)r\neg(p \land q) \lor r \equiv (\neg p \lor \neg q) \lor r
Step 2: Since disjunction is associative, flatten the expression into a single clause.
¬p¬qr\equiv \neg p \lor \neg q \lor r
Answer: The CNF is ¬p¬qr\neg p \lor \neg q \lor r, which is a single clause (a conjunction of one clause).

Why It Matters

CNF is the required input format for SAT solvers, which are algorithms that determine whether a logical formula can be satisfied. It also appears in resolution-based proof systems in discrete math and artificial intelligence courses. Understanding CNF is essential for automated theorem proving and constraint satisfaction problems.

Common Mistakes

Mistake: Confusing CNF with Disjunctive Normal Form (DNF). Students sometimes distribute AND over OR instead of OR over AND.
Correction: In CNF, the outer connective is AND and each clause uses OR. In DNF, it is the reverse: OR of AND-clauses. When converting, distribute \lor over \land, not the other way around.