First, we define a literal to be either a propositional letter or its negation, e.g. or .
To put a formula into Conjunctive Normal Form (CNF), do the following three steps:
But this last step can lead to an exponential blow-up. For example, consider the formula .
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:
Create new variables, , 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:
This new formula may not be equivalent to original formula: Suppose that the original formula is satisfiable and let be a valuation that satisfies it. Extend to by setting to false for each . Then the new formula evaluates to false under although the original formula is still true under .
On the other hand if the original formula is satisfiable, then the new formula is also, and visa versa. Say that satisfies the original formula. Extending to by setting to the value of for each 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.