Rudy’s OBTF Rudolf Adamkovič

Home / Computer science / 3-satisfiability (3SAT) / Explore / Case 4: More than three literals / Proof / Case 1: \(c\) is satisfiable


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

© 2025 Rudolf Adamkovič under GNU General Public License version 3.
Made with Emacs and secret alien technologies of yesteryear.