Rudy’s OBTF Rudolf Adamkovič

Home / Computer science / 3-satisfiability (3SAT) / Explore


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

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