## § 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*.