Up: Computational problem [Top][Contents]

3SAT

a.k.a.

3-satisfiability

Define

… as a special case of SAT with

exactly three literals per clause.

Explore

… polynomial-time reduction from SAT,

proving NP-completeness of 3SAT.

For each clause \(c\) in a SAT instance,

Case 1: One literal

The one-literal clause

\[\begin{equation*}
  c = (\ell)
\end{equation*}
\]

becomes four three-literal clauses

\[\begin{align*}
  c'_1 & = (\ell \lor \hphantom{\lnot} y_1 \lor \hphantom{\lnot} y_2) \\
  c'_2 & = (\ell \lor \hphantom{\lnot} y_1 \lor \lnot y_2) \\
  c'_3 & = (\ell \lor \lnot y_1 \lor \hphantom{\lnot} y_2) \\
  c'_4 & = (\ell \lor \lnot y_1 \lor \lnot y_2).
\end{align*}
\]

Proof

By truth tables, with

\[\begin{equation*}
  c' = (c'_1 \land c'_2 \land c'_3 \land c'_4),
\end{equation*}
\]

we have

\[\begin{align*}
  \begin{array}{ccc|ccccc}
    c & y_1 & y_2 & c'_1 & c'_2 & c'_3 & c'_4 & c' \\[1ex]
    \boxed{0} & 0 & 0 & 0 & 1 & 1 & 1 & \boxed{0} \\[0.25ex]
    \boxed{0} & 0 & 1 & 1 & 0 & 1 & 1 & \boxed{0} \\[0.25ex]
    \boxed{0} & 1 & 0 & 1 & 1 & 0 & 1 & \boxed{0} \\[0.25ex]
    \boxed{0} & 1 & 1 & 1 & 1 & 1 & 0 & \boxed{0} \\[0.25ex]
    \boxed{1} & 0 & 0 & 1 & 1 & 1 & 1 & \boxed{1} \\[0.25ex]
    \boxed{1} & 0 & 1 & 1 & 1 & 1 & 1 & \boxed{1} \\[0.25ex]
    \boxed{1} & 1 & 0 & 1 & 1 & 1 & 1 & \boxed{1} \\[0.25ex]
    \boxed{1} & 1 & 1 & 1 & 1 & 1 & 1 & \boxed{1} \\[0.25ex]
  \end{array} \> \> .
\end{align*}
\]

\(\blacksquare\)

Case 2: Two literals

The two-literal clause

\[\begin{equation*}
  c = (\ell_1 \lor \ell_2)
\end{equation*}
\]

becomes two three-literal clauses

\[\begin{align*}
  c'_1 & = ( \ell_1 \lor \ell_2 \lor \hphantom{\lnot} y ) \\
  c'_2 & = ( \ell_1 \lor \ell_2 \lor \lnot y ).
\end{align*}
\]

Proof

By truth tables, with

\[\begin{equation*}
  c' = (c'_1 \land c'_2),
\end{equation*}
\]

we have

\[\begin{align*}
  \begin{array}{ccc|cccc}
    \ell_1 & \ell_2 & y & c & c'_1 & c'_2 & c' \\[1ex]
    0 & 0 & 0 & \boxed{0} & 0 & 1 & \boxed{0} \\[0.25ex]
    0 & 0 & 1 & \boxed{0} & 1 & 0 & \boxed{0} \\[0.25ex]
    0 & 1 & 0 & \boxed{1} & 1 & 1 & \boxed{1} \\[0.25ex]
    0 & 1 & 1 & \boxed{1} & 1 & 1 & \boxed{1} \\[0.25ex]
    1 & 0 & 0 & \boxed{1} & 1 & 1 & \boxed{1} \\[0.25ex]
    1 & 0 & 1 & \boxed{1} & 1 & 1 & \boxed{1} \\[0.25ex]
    1 & 1 & 0 & \boxed{1} & 1 & 1 & \boxed{1} \\[0.25ex]
    1 & 1 & 1 & \boxed{1} & 1 & 1 & \boxed{1} \\[0.25ex]
  \end{array} \> \> .
\end{align*}
\]

\(\blacksquare\)

Case 3: Three literals

The 3-literal clause

\[\begin{equation*}
  c = ( \ell_1 \lor \ell_2 \lor \ell_3 )
\end{equation*}
\]

stays as is.

Case 4: More than three literals

The \((k > 3)\)-literal clause

\[\begin{equation*}
  c = ( \ell_1, \ell_2, \ell_3, \ldots, \ell_k )
\end{equation*}
\]

becomes \(k - 2\) three-literal clauses

\[\begin{align*}
  c'_1 & = (\hphantom{\lnot} \ell_1 \lor \ell_2 \lor y_1) \\
  c'_2 & = (\lnot y_1 \lor \ell_3 \lor y_2) \\
  c'_3 & = (\lnot y_2 \lor \ell_4 \lor y_3) \\[1ex]
  \vdots & \\[1ex]
  c'_k & = (\lnot y_{k - 5} \lor \ell_{k - 3} \lor y_{k - 4}) \\
  c'_{k - 1} & = (\lnot y_{k - 4} \lor \ell_{k - 2} \lor y_{k - 3}) \\
  c'_{k - 2} & = (\lnot y_{k - 3} \lor \ell_{k - 1} \lor \ell_k)
\end{align*}
\]

Proof

Case 1: \(c\) is satisfiable

Case 1A: \(\ell_1 = 1\) or \(\ell_2 = 1\)

Setting

\[\begin{equation*}
  y_i = 0 \quad \forall i
\end{equation*}
\]

satisfies all clauses:

\[\begin{align*}
  c'_1
  & = (\ell_1 \lor \ell_2 \lor y_1) \\
  & = (\boxed{\ell_1} \lor \boxed{\ell_2} \lor 0) \\
  & = 1 \\[2ex]
  c'_2
  & = (\lnot y_1 \lor \ell_3 \lor y_2) \\
  & = (\boxed{\lnot 0} \lor \ell_3 \lor 0) \\
  & = 1 \\[1ex]
  & \vdots \\[2ex]
  c'_{k - 1}
  & = (\lnot y_{k - 4} \lor \ell_{k - 2} \lor y_{k - 3}) \\
  & = (\boxed{\lnot 0} \lor \ell_{k - 2} \lor 0) \\
  & = 1 \\[2ex]
  c'_{k - 2}
  & = (\lnot y_{k - 3} \lor \ell_{k - 1} \lor \ell_k) \\
  & = (\boxed{\lnot 0} \lor \ell_{k - 2} \lor \ell_k) \\
  & = 1.
\end{align*}
\]

Case 1B: \(\ell_{k - 1} = 1\) or \(\ell_k = 1\)

Setting

\[\begin{equation*}
  y_i = 1 \quad \forall i
\end{equation*}
\]

satisfies all clauses:

\[\begin{align*}
  c'_1
  & = (\ell_1 \lor \ell_2 \lor y_1) \\
  & = (\ell_1 \lor \ell_2 \lor \boxed{1}) \\
  & = 1 \\[2ex]
  c'_2
  & = (\lnot y_1 \lor \ell_3 \lor y_2) \\
  & = (\lnot 1 \lor \ell_3 \lor \boxed{1}) \\
  & = 1 \\[1ex]
  \vdots & \\[2ex]
  c'_{k - 1}
  & = (\lnot y_{k - 4} \lor \ell_{k - 2} \lor y_{k - 3}) \\
  & = (\lnot 1 \lor \ell_{k - 2} \lor \boxed{1}) \\
  & = 1 \\[2ex]
  c'_{k - 2}
  & = (\lnot y_{k - 3} \lor \ell_{k - 1} \lor \ell_k) \\
  & = (\lnot 1 \lor \boxed{\ell_{k - 1}} \lor \boxed{\ell_k}) \\
  & = 1.
\end{align*}
\]

Case 1C: \(\ell_i = 1\) with \(i \not\in \{1, 2, k - 1, k\}\)

Setting

\[\begin{equation*}
  y_j =
  \begin{cases}
  1 & \text{for} \quad 1 \leq j \leq i - 2 \\
  0 & \text{for} \quad i - 1 \leq j \leq y_{k - 3}
  \end{cases}
\end{equation*}
\]

satisfies all clauses:

\[\begin{align*}
  c'_1
  & = (\ell_1 \lor \ell_2 \lor  y_1) \\
  & = (\ell_1 \lor \ell_2 \lor \boxed{1}) \\
  & = 1 \\[2ex]
  c'_2
  & = (\lnot y_1 \lor \ell_3 \lor y_2) \\
  & = (\lnot 1 \lor \ell_3 \lor \boxed{1}) \\
  & = 1 \\[1ex]
  \vdots & \\[2ex]
  c'_{i - 1}
  & = (\lnot y_{i - 2} \lor \ell_i \lor y_{i - 1}) \\
  & = (\lnot 1 \lor \boxed{1} \lor 0) \\
  & = 1 \\[1ex]
  \vdots & \\[2ex]
  c'_{k - 1}
  & = (\lnot y_{k - 4} \lor \ell_{k - 2} \lor y_{k - 3}) \\
  & = (\boxed{\lnot 0} \lor \ell_{k - 2} \lor 0) \\
  & = 1 \\[2ex]
  c'_{k - 2}
  & = (\lnot y_{k - 3} \lor \ell_{k - 1} \lor \ell_k) \\
  & = (\boxed{\lnot 0} \lor \ell_{k - 1} \lor \ell_k) \\
  & = 1.
\end{align*}
\]

Case 2: \(c\) is not satisfiable

For all \(i\), \(\ell_i = 0\).

Case 2A: \(y_1 = 0\)

The first clause is not satisfied:

\[\begin{align*}
  c'_1
  & = (\ell_1 \lor \ell_2 \lor y_1) \\
  & = (0 \lor 0 \lor \boxed{0}) \\
  & = 0 \\[1ex]
  \vdots &
\end{align*}
\]

Case 2B: \(y_1 = 1\)

To make all clauses satisfied

\[\begin{equation*}
  y_1 = 1 \implies y_2 = 1 \implies \cdots \implies y_{k - 3} = 1
\end{equation*}
\]

but then the last clause is not satisfied:

\[\begin{align*}
  c'_1
  & = (\ell_1 \lor \ell_2 \lor y_1) \\
  & = (0 \lor 0 \lor \boxed{1}) \\
  & = 1 \\[1ex]
  \vdots & \\[2ex]
  c'_{k - 1}
  & = (\lnot y_{k - 4} \lor \ell_{k - 2} \lor y_{k - 3}) \\
  & = (\lnot \boxed{1} \lor 0 \lor \boxed{1}) \\
  & = 1 \\[2ex]
  c'_{k - 2}
  & = (\lnot y_{k - 3} \lor \ell_{k - 1} \lor \ell_k) \\
  & = (\lnot \boxed{1} \lor 0 \lor 0) \\
  & = 0.
\end{align*}
\]

\(\blacksquare\)