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

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