This slideshow shows how to convert (reduce) a general instance of the Formula Satisfiability problem to a version with exactly 3 literals in every clause (so as to be a valid input to the 3-CNF Satisfiability problem) in polynomial time

Consider a general input to SAT: $C_1 . C_2 . \cdots . C_n$. Each clause must be one of the following four cases.

 1. It contains three literals. For example: ($x_1 + \overline{x_2} + x_3$).
      No reduction is needed for this case.

 2. It contains only one literal. For example: ($x_1$).

 3. It contains two literals. For example: ($x_1 + \overline{x_2}$).

 4. It contains more than three literals. For example: $(x_1 + \overline{x_2} + x_3 \cdots + x_k)$ where $k > 3$.

We now show how a clause $C$ from any of the cases above can be replaced by a collection of one or more clauses ($Z$) such that:
1. All clauses in $Z$ contain exactly 3 literals.
2. $C$ is satisfiable if and only if $Z$ is satisfiable.

Let $C_i = l_i$ where $l_i$ is a literal.

Introduce 2 new variables $y_{i,1}$ and $y_{i,2}$.

Replace $C_i$ by $Z_i$, a conjunction of four clauses, where

$Z_i =$

$(l_i + y_{i,1} + y_{i,2}) \cdot$

$(l_i + \overline{y_{i,1}} + y_{i,2})\ \cdot$

$(l_i + y_{i,1} + \overline{y_{i,2}})\ \cdot$

$(l_i + \overline{y_{i,1}} + \overline{y_{i,2}})$.

I

II

III

IV

When $C_i$ (i.e. $l_i$) is $True$, $Z_i$ is true.

When $C_i$ (i.e. $l_i$) is $False$, $Z_i$ is false.

Hence $C_i$ can be reduced to $Z_i$ where each clause in $Z_i$ contains exactly 3 literals and $C_i \iff Z_i$.

Let $C_i$ = ($l_{i,1}$ + $l_{i,2}$) where $l_{i,1}$ and $l_{i,2}$ are literals.

Introduce a new variable $y_i$.

Replace $C_i$ by conjunction of clauses $Z_i$ where

$\ \ Z_i = (l_{i,1} + l_{i,2} + y_i) \cdot (l_{i,1} + l_{i,2} + \overline{y_i})$.

I

II

When $C_i$ is true, $Z_i$ is true.

When $C_i$ is false, $Z_i$ is false.

Hence $C_i$ can be reduced to $Z_i$ where each clause in $Z_i$ contains exactly 3 literals and $C_i \iff Z_i$.

Let $C_i = (l_{i,1} + l_{i,2} + l_{i,3} + \cdots + l_{i,k})$ where $k > 3$.

Introduce $k-3$ new variables: $y_1 , y_2, \cdots ,y_{k-3}$.

Replace $C_i$ with a sequence of clauses $Z_i$ where

$Z_i = (l_{i,1} + l_{i,2} + y_1) \cdot (\overline{y_1} + l_{i,3} + y_2) \cdots (\overline{y_{j-2}} + l_{i,j} + y_{j-1}) \cdots (\overline{y_{k-4}} + l_{i,k-2} + y_{k-3}) \cdot(\overline{y_{k-3}} + l_{i,k-1} + l_{i,k})$.

We need to prove:

a. When $C_i$ is satisfiable,$Z_i$ is satisfiable.

b. When $C_i$ is not satisfiable, $Z_i$ is not satisfiable.

$C_i = (l_{i,1} + l_{i,2} + l_{i,3} + \cdots + l_{i,k})$ where $k > 3$.

$Z_i =$

$($

$l_{i,1} + l_{i,2}$

$+$

$y_1$

$)\cdot($

$\overline{y_1}$

$+$

$l_{i,3}$

$+$

$y_2$

$) \cdots ($

$\overline{y_{j-3}}$

$+$

$l_{i,j-1}$

$+$

$y_{j-2}$

$)\cdot($

$\overline{y_{j-2}}$

$+$

$l_{i,j}$

$+$

$y_{j-1}$

$)\cdot($

$\overline{y_{j-1}}$

$+$

$l_{i,j+1}$

$+$

$y_{j}$

$)\cdots($

$\overline{y_{k-4}}$

$+$

$l_{i,k-2}$

$+$

$y_{k-3}$

$)\cdot$

$($

$\overline{y_{k-3}}$

$+$

$l_{i,k-1} + l_k$

$)$

When $C_i$ is satisfiable, at least one literal in ${l_{i,1} ... l_{i,k}}$ is $True$.

If any of $l_{i,1}$ or $l_{i,2}$ is $True$, set all the additional variables $y_1 ,y_2 \cdots y_{k-3}$ to $False$.

The first term of all the clauses in $Z_i$ other than the first has a literal $\overline{y_n}$ which evaluates to $True$.

If any of $l_{i,k-1}$ or $l_{i,k}$ is $True$, set all the additional variables $y_1 ,y_2 \cdots y_{k-3}$ to $True$.

The third term of all the clauses in $Z_i$ other than the last has a literal $y_n$ which evaluates to $True$.

If $l_{i,j}$ $(where \ j \notin \{1,2,k-1,k\})$ is $True$, set $y_1 \cdots y_{j-2}$ to $True$ and $y_{j-1} \cdots y_{k-3}$ to $False$.

Let us call the clause in $Z_i$ containing $l_{i,j}$ in as $C$'.

--------------------

$C'$

The third term of all the clauses in $Z_i$ left to $C'$ has a literal $y_n$ ($where \ n \in \{1..j-2\}$) which evaluates to $True$.

The first term of all the clauses in $Z_i$ right to $C'$ has a literal $\overline{y_n}$ ($where \ n \in \{j-1..k-3\}$) which evaluates to $True$.

Hence when $C_i$ is satisfiable, $Z_i$ is satisfiable.

When $C_i$ is not satisfiable, NO literal in { $l_i,1 \cdots l_i,k$ } is $True$.

For $Z_i$ to be satisfiable, all its clauses must evaluate to $True$.

For the first clause to be $True$, $y_1 = True.$

Now for the second clause to be $True$, $y_2 = True$.

Similarly for the third clause to be $True$, $y_3 = True$.

$y_3 = True \Rightarrow y_4 = True \cdots \Rightarrow y_{j-2} = True \Rightarrow y_{j-1} = True \Rightarrow y_j = True \cdots \Rightarrow y_{k-4} = True \Rightarrow y_{k-3} = True$.

The last clause evaluates to $False$. Hence $Z_i$ is NOT SATISFIABLE.

Hence we have proved:

a. When $C_i$ is satisfiable., $Z_i$ is satisfiable

b. When $C_i$ is not satisfiable., $Z_i$ is not satisfiable

Hence any clause in a SAT expression can be replaced by a conjunction of clauses which contain 3 literals each.


Therefore, an instance of SAT can be reduced to an equivalent instance of 3-SAT in polynomial time.