Explore

• 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\)