Rudy’s OBTF Rudolf Adamkovič

Home / Computer science / 3-satisfiability (3SAT) / Explore / Case 1: One literal


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


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