Home / Computer science / 3-satisfiability (3SAT) / Explore / Case 4: More than three literals / Proof / Case 2: \(c\) is not satisfiable
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\)