Home / Computer science / 3-satisfiability (3SAT) / Explore
Case 2: Two literals
The two-literal clause
\begin{equation*} c = (\ell_1 \lor \ell_2) \end{equation*}becomes two three-literal clauses
\begin{align*} c'_1 & = ( \ell_1 \lor \ell_2 \lor \hphantom{\lnot} y ) \\ c'_2 & = ( \ell_1 \lor \ell_2 \lor \lnot y ). \end{align*}