Home / Computer science / 3-satisfiability (3SAT) / Explore
Case 1: One literal
The one-literal clause
\begin{equation*} c = (\ell) \end{equation*}becomes four three-literal clauses
\begin{align*} c'_1 & = (\ell \lor \hphantom{\lnot} y_1 \lor \hphantom{\lnot} y_2) \\ c'_2 & = (\ell \lor \hphantom{\lnot} y_1 \lor \lnot y_2) \\ c'_3 & = (\ell \lor \lnot y_1 \lor \hphantom{\lnot} y_2) \\ c'_4 & = (\ell \lor \lnot y_1 \lor \lnot y_2). \end{align*}