§ 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 xx and ¬x\lnot x are in the same SCC, we don't have a solution, because this means that true=false\texttt{true} = \texttt{false} or false=true\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 xx and ¬x\lnot x are in two different components. So this means that we have the possible orderings
  • x    ¬xx \implies \lnot x: true    false\texttt{true} \implies \texttt{false} (Inconsistent!)
  • x    ¬xx \implies \lnot x: false    true\texttt{false} \implies \texttt{true} (Consistent, principle of explosion)
Hence, if xx implies ¬x\lnot x, we should set xx to false\texttt{false}. The other assignment is inconsistent .