Conjunctive Normal Form

First, we define a literal to be either a propositional letter or its negation, e.g. $p$ or $\neg p$.

To put a formula into Conjunctive Normal Form (CNF), do the following three steps:

1. Remove all implication operators ($\rightarrow$) by replacing all formulas of the form $\phi \rightarrow \psi$ with $\neg \phi \vee \psi$.

2. Push the not operators ($\neg$) into the formulas as far as possible by using DeMorgan's laws:
   • $\neg \neg \phi$ becomes $\phi$.
   • $\neg (\phi \wedge \psi)$ becomes $(\neg \phi \vee \neg \psi)$.
   • $\neg (\phi \vee \psi)$ becomes $(\neg \phi \wedge \neg \psi)$.

3. Move all conjunctions ($\wedge$) outside of the disjunctions ($\vee$) by using distributivity repeatedly:
   • $(\phi \wedge \psi) \vee \xi$ becomes $(\phi \vee \xi) \wedge (\psi \vee \xi)$.
   • $\phi \vee (\psi \wedge \xi)$ becomes $(\phi \vee \psi) \wedge (\phi \vee \xi)$.

But this last step can lead to an exponential blow-up. For example, consider the formula $(p_1 \wedge q_1) \vee (p_2 \wedge q_2) \vee \ldots \vee (p_n \wedge q_n)$.

There is a method which constructs a formula in CNF that is satisfiable if and only if the original formula is satisfiable without the exponential blow-up. Suppose that after removing the implication operators and pushing negation in as far as possible, we have a disjunction:

$$(\phi_{1,1} \wedge \phi_{1,2} \wedge \ldots \wedge \phi_{1,n_... ...phi_{m,1} \wedge \phi_{m,2} \wedge \ldots \wedge \phi_{m,n_m}).$$

Create new variables, $x_1, \ldots, x_m$, one for each disjunct, replace each disjunct with the corresponding variable, and conjoin this new formula with formulas that state the equivalence of the new variables to their corresponding formulas. In this case, we have:

$$\begin{eqnarray*} (x_1 \vee x_2 \vee \ldots \vee x_m) & \wedge & (x_1 \rightar... ... \phi_{m,2} \wedge \ldots \wedge \phi_{m,n_m}) \rightarrow x_m) \end{eqnarray*}$$

This new formula may not be equivalent to original formula: Suppose that the original formula is satisfiable and let $E$ be a valuation that satisfies it. Extend $E$ to $E'$ by setting $x_i$ to false for each $i$. Then the new formula evaluates to false under $E'$ although the original formula is still true under $E'$.

On the other hand if the original formula is satisfiable, then the new formula is also, and visa versa. Say that $E$ satisfies the original formula. Extending $E$ to $E'$ by setting $x_i$ to the value of $(\phi_{i,1} \wedge \phi_{i,2} \wedge \ldots \wedge \phi_{i,n_i})$ for each $i$ yields a valuation that satisfies the new formula. Any valuation that satisfies the new formula will also satisfy the old one.

The result of putting this new formula into CNF is an expression that is a constant times the size of the original formula.

This also means the original formula is unsatisfiable if and only if the new formula is unsatisfiable. This is the property that we need for the resolution procedure (see below) to operate correctly.