This slideshow presents how to reduce a Formula Satisfiability problem to an 3 CNF Satisfiability problem in polynomial time

There can be only four cases for a clause in a SAT formula : $C_1$   . $C_2$ . $\cdots$ . $C_n$

Let $C_i$ denote a random clause in a SAT formula where $i$ can range from 1 to n

 1. It contains three literals.     For example : ($x_1 + \overline{x_2} + x_3$)
    No reduction 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$

Any of the above type of clause (C) can be replaced by a conjunction of clauses (Z) such that

1. All clauses in Z contain exactly 3 literals.

2. C is satisfiable if and only if Z is satisfiable. that is $C \iff Z$

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 conjunction of clauses $Z_i$ 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})$

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}$

$)$

$($

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

$+$

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

$)$

When $C_i$ is satisfiable atleast 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 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 contains 3 literals each.


So, a SAT problem can be reduced to an instance of 3-SAT in polynomial time.