Clauses as implications
A 2 SAT problem is a boolean formula where every clause has two literals. Each clause that one of two literals must be true is equivalent to two implications: if the first is false then the second is true, and if the second is false then the first is true.
The implication graph
Build a directed graph with two nodes per variable, one for the variable being true and one for it being false. Add an edge for each implication. The formula is satisfiable if and only if no variable has its true node and its false node in the same strongly connected component.
- Convert each clause into two implication edges.
- Find strongly connected components.
- Unsatisfiable when a variable and its negation share a component.
To extract an assignment, order components topologically and set each variable by which of its two nodes appears later.
Key idea
2 SAT reduces to an implication graph where each clause becomes two edges, and it is satisfiable exactly when no variable shares a strongly connected component with its own negation.