Application: 2-SAT Connection

$2$-SAT (Boolean satisfiability with two literals per clause) problems use SCC detection to check if a solution exists. Build an implication graph where each variable $x$ has two nodes: $x$ and $eg x$ (not $x$).

For each clause, add implication edges. If $x$ and $eg x$ end up in the same SCC, no satisfying assignment exists. If they are in different SCCs, a solution exists.

Assign truth values based on the topological order of SCCs in the condensation graph. You will see this technique in detail in the next section.