SKEDSOFT

3-CNF, =-satisfiability, and general CNF: A 3-CNF formula is a CNF formula in which every clause has three literals. For example,

is a 3-CNF formula. As can be seen, there is no requirement on what variables the clauses might involve. Many proofs are rendered easier by standardizing on the 3-CNF form.
In many proofs, it will be handy to restrict the satisfying assignments allowed. One useful form of this restriction is the =-satisfiability restriction. Given a 3-CNF formula, a =-assignment is one under which every clause has two literals with unequal truth values. Given a set of N clauses where the ith clause is ci = yi1 ∨ yi2 ∨ yi3, suppose we transform each such clause into two clauses by introducing a new variable zi per original clause, and a single variable b for the whole translation:

We can show that for any given formula Fmla = ∧i∈Nci, the above described transformation is a polynomial-time mapping reduction ≤P from 3-SAT to =-sat.
Finally, a general CNF formula is one where the number of literals in each clause can vary. A conversion from general CNF to 3-CNF that does not increase the length of the formula beyond a polynomial factor and takes no more than polynomial-time is now described (for each clause with less than 3 literals, replicating some literal can increase its size to 3; e.g., (a∨b) = (a∨b∨b)). Consider a clause with l literals:

This clause can be rewritten into one with l − 2 clauses:

Applying these transformations to a general CNF formula results in one that is equivalent as far as satisfiability goes. This is known as equi-satisfiable.