11.33

Algorithm overview
1. For every clause [math]\displaystyle{ (a \lor b) }[/math] create the two implications     [math]\displaystyle{ (\lnot a \;\Rightarrow\; b) }[/math] and [math]\displaystyle{ (\lnot b \;\Rightarrow\; a) }[/math].
2. Let G be the directed “implication graph’’ on the [math]\displaystyle{ 2n }[/math] literals     [math]\{x_1,\lnot x_1,\dots ,x_n,\lnot x_n\}[/math] containing all these edges.
3. Compute the strongly-connected components (SCCs) of G with e.g. Kosaraju or Tarjan (linear time).
4. Unsatisfiable iff some variable and its negation belong to the same SCC.
5. Otherwise obtain a satisfying assignment by condensing G to its SCC-DAG, processing the components in reverse topological order and setting a variable true the first time either it or its negation is encountered.

Correctness sketch
• Each implication encodes exactly the semantics of its clause, so any truth assignment that satisfies the formula respects all edges of G.
• If [math]\displaystyle{ x }[/math] and [math]\displaystyle{ \lnot x }[/math] lie in the same SCC then both [math]\displaystyle{ x\Rightarrow\lnot x }[/math] and [math]\displaystyle{ \lnot x\Rightarrow x }[/math] are reachable, forcing the contradictory requirements “x is true” and “x is false’’ – impossible.
• Conversely, when no such conflict exists we can orient the SCC-DAG so that a literal and its negation are never in the same or later component, yielding the assignment produced in Step 5, which satisfies every implication and thus every clause.

Complexity
Building the graph uses two edges per clause, so [math]\displaystyle{ O(m) }[/math] where [math]\displaystyle{ m }[/math] is the number of clauses; SCC computation is [math]\displaystyle{ O(n+m) }[/math]. Hence 2-SAT is solvable in linear time.

Pseudocode

function twoSAT(n, clauses): G ← directed graph with 2n vertices for (a ∨ b) in clauses: addEdge(¬a, b) ; addEdge(¬b, a) sccID ← stronglyConnectedComponents(G) for each variable x_i: if sccID[x_i] == sccID[¬x_i]: return UNSATISFIABLE order ← topologicalOrderOfSCCDAG(G, sccID) assignment ← array[1..n] for v in order (reverse): lit ← literal represented by v var ← variable of lit if assignment[var] is unset: assignment[var] ← (lit is positive) return SATISFIABLE, assignment

Back to Chapter 11