§ 2-SAT

First break into SCC's. Each SCC represents equivalence: since there is a path from every variable to every other variable, they must take on the exact same value. Hence if $x$ and $\lnot x$ are in the same SCC, we don't have a solution, because this means that $\texttt{true} = \texttt{false}$ or $\texttt{false} = \texttt{true}$. Let's say we find SCC's where this does not happen. Now, zoom out and think of the condensation DAG. We want to assign true/false to each node in the SCC DAG. How should we assign true/false? Say that $x$ and $\lnot x$ are in two different components. So this means that we have the possible orderings

• $x \implies \lnot x$: $\texttt{true} \implies \texttt{false}$ (Inconsistent!)
• $x \implies \lnot x$: $\texttt{false} \implies \texttt{true}$ (Consistent, principle of explosion)

Hence, if $x$ implies $\lnot x$, we should set $x$ to $\texttt{false}$. The other assignment is inconsistent .