Lab 10 — Strongly Connected Components & 2-SAT

Goal

Implement Tarjan’s one-pass SCC algorithm iteratively (explicit stack — mandatory in Python at n = 10⁵), understand the condensation DAG, and apply SCC to its killer application: 2-SAT in O(n + m) with assignment extraction. After this lab: iterative Tarjan in <20 minutes, the 2-SAT reduction from memory in <10.

Background Concepts

An SCC is a maximal set of mutually reachable vertices. Tarjan finds all of them in one DFS using two numbers per vertex: disc[v] (discovery time) and low[v] = min disc reachable from v’s subtree using any number of tree edges plus at most one edge into a still-open SCC.

Stack invariant: vertices are pushed on a side stack at discovery and popped only when their SCC’s root closes. A vertex stays on the stack exactly while its SCC is still open — i.e., it can still reach an earlier unfinished vertex. When DFS finishes v with low[v] == disc[v], v is the first-discovered vertex (root) of its SCC, and its SCC is precisely v plus everything above it on the stack. Pop them together.

Because an SCC closes only after every SCC it reaches has closed, Tarjan emits SCCs in reverse topological order — component ids double as a reverse topo sort for free.

Kosaraju is the two-pass alternative: DFS once recording finish order, then DFS the reversed graph in decreasing finish order; each second-pass tree is one SCC. Easier to re-derive under pressure, but needs the reverse graph and two passes.

Condensation: contract each SCC to one node → a DAG. Every DAG technique now applies: topo-order DP, longest path, reachability.

2-SAT: variables x₀..x_{n−1}, clauses (a ∨ b). Each clause is two implications: ¬a→b and ¬b→a (twin edges — always both). Build this implication graph on 2n literal-vertices. The formula is satisfiable iff no variable shares an SCC with its negation. A valid assignment: set each literal true iff its SCC comes later in topological order than its negation’s.

Interview Context

SCC is a staple at trading firms and infra teams (deadlock detection, dependency cycles). 2-SAT appears disguised as “pairwise constraints: pick one of two options per item, some pairs conflict — feasible?” Recognizing the implication-graph reduction is a senior-level signal. LC has no direct 2-SAT problem (stated honestly below); Codeforces and interviews at HFT shops do. Course Schedule (LC 207/210) is the condensation warm-up; don’t confuse LC 1192 (Critical Connections) — that’s bridges, the undirected twin, next lab.

Problem Statement

2-SAT (Codeforces-style; LeetCode has no canonical 2-SAT problem — this is the honest framing). Given n_vars boolean variables and m clauses, each (l₁ ∨ l₂) where a literal is a variable or its negation, decide satisfiability and return one satisfying assignment or report none. Literal encoding: 2v = x_v, 2v+1 = ¬x_v; negation is lit ^ 1.

Constraints

  • 1 ≤ n_vars, m ≤ 10⁵ → implication graph has 2·10⁵ vertices, 2m edges.
  • O(n + m) required; recursion depth may hit 2·10⁵ → iterative DFS.

Clarifying Questions

  1. Exactly two literals per clause? (Yes — three makes it 3-SAT, NP-complete.)
  2. May a clause repeat a literal, e.g. (x ∨ x)? (Yes — it forces x true; the twin edges handle it.)
  3. One assignment, all, or a count? (One; counting solutions is #P-complete.)
  4. Any satisfying assignment, or lexicographically smallest? (Any — lex-smallest needs a different, greedy technique.)

Examples

# (x0 ∨ x1) ∧ (¬x0 ∨ x1) ∧ (¬x1 ∨ x2)
solve_2sat(3, [(0, 2), (1, 2), (3, 4)]) → [False, True, True]  (one valid answer)

# x0 ∧ ¬x0, encoded as (x0 ∨ x0) ∧ (¬x0 ∨ ¬x0)
solve_2sat(1, [(0, 0), (1, 1)]) → None

Initial Brute Force

Enumerate all 2ⁿ assignments; check every clause for each.

Brute Force Complexity

O(2ⁿ · m). Unusable past n ≈ 25; at n = 10⁵, astronomically dead.

Optimization Path

Key observation: (a ∨ b) ≡ (¬a → b) ∧ (¬b → a). Chains of implications are paths; “x forces ¬x and ¬x forces x” is exactly “x and ¬x mutually reachable” — one SCC. So satisfiability reduces to SCC computation: Tarjan (one pass) or Kosaraju (two passes), both O(n + m). No search, no DPLL — 2-SAT is polynomial precisely because clauses are binary implications.

Final Expected Approach

def tarjan_scc(n, adj):
    """Iterative Tarjan. Returns (count, comp); comp ids are assigned in
    reverse topological order: edge u→v across SCCs ⇒ comp[u] > comp[v]."""
    UNSEEN = -1
    disc = [UNSEEN] * n
    low = [0] * n
    on_stk = [False] * n
    comp = [UNSEEN] * n
    stk, work = [], []
    timer = count = 0
    for s in range(n):
        if disc[s] != UNSEEN:
            continue
        work.append((s, 0))
        while work:
            v, i = work[-1]
            if i == 0:                            # first visit
                disc[v] = low[v] = timer
                timer += 1
                stk.append(v)
                on_stk[v] = True
            if i < len(adj[v]):
                work[-1] = (v, i + 1)
                w = adj[v][i]
                if disc[w] == UNSEEN:
                    work.append((w, 0))           # tree edge: recurse
                elif on_stk[w]:
                    low[v] = min(low[v], disc[w])  # back/cross into open SCC
            else:                                 # v is finished
                work.pop()
                if work:
                    low[work[-1][0]] = min(low[work[-1][0]], low[v])
                if low[v] == disc[v]:             # v is its SCC's root
                    while True:
                        w = stk.pop()
                        on_stk[w] = False
                        comp[w] = count
                        if w == v:
                            break
                    count += 1
    return count, comp

def solve_2sat(n_vars, clauses):
    """clauses: list of (l1, l2) meaning l1 ∨ l2.
    Literal encoding: 2v = x_v, 2v+1 = ¬x_v; negate with lit ^ 1.
    Returns a satisfying list of bools, or None."""
    adj = [[] for _ in range(2 * n_vars)]
    for a, b in clauses:
        adj[a ^ 1].append(b)                      # ¬a → b
        adj[b ^ 1].append(a)                      # ¬b → a
    _, comp = tarjan_scc(2 * n_vars, adj)
    assign = []
    for v in range(n_vars):
        if comp[2 * v] == comp[2 * v + 1]:
            return None                           # x and ¬x entangled
        # smaller comp id = later in topo order = "chosen" literal
        assign.append(comp[2 * v] < comp[2 * v + 1])
    return assign

Data Structures Used

  • Adjacency lists over 2·n_vars literal-vertices.
  • disc, low, comp int arrays; on_stk boolean array.
  • Two explicit stacks: work holds (vertex, next-edge-index) frames (the recursion replacement); stk is Tarjan’s SCC stack.

Correctness Argument

Root detection: low[v] == disc[v] after v’s subtree finishes means no vertex in the subtree reaches an earlier open vertex. So v’s SCC is entirely within the stack segment above v (everything pushed after v that couldn’t escape below it) — pop it as one component. Induction over pop order makes each popped set maximal.

Reverse topo ids: if SCC A has an edge into SCC B (A→B, A ≠ B), DFS finishes B’s root strictly before A’s — so comp[B] < comp[A]. Verified as an explicit edge-property check in the tests.

2-SAT, necessity: x and ¬x in one SCC gives x→¬x and ¬x→x — either value of x forces its own negation. UNSAT.

2-SAT, sufficiency of the assignment rule: the implication graph is skew-symmetric — every edge l→l′ has a mirror ¬l′→¬l. Rule: literal l is chosen iff comp[l] < comp[¬l]. Suppose a chosen l implies a rejected l′: then comp[l] ≥ comp[l′] (edge, reverse-topo ids) and, by the mirror edge ¬l′→¬l, comp[¬l′] ≥ comp[¬l]. Chain: comp[¬l] ≤ comp[¬l′] < comp[l′] ≤ comp[l] < comp[¬l] — contradiction. So the chosen set is closed under implication and hits exactly one of each pair: every clause’s implications are satisfied.

Complexity

StepTimeSpace
Build implication graphO(n + m)O(n + m)
Tarjan SCCO(n + m)O(n)
Extract assignmentO(n)O(n)

Implementation Requirements

  • Iterative DFS is non-negotiable: 2·10⁵ recursion depth kills Python even with sys.setrecursionlimit (the C stack overflows before the Python limit triggers).
  • The i == 0 guard must gate the first-visit block — frames are re-entered after each child.
  • on_stk check before using disc[w]: edges into closed SCCs must not update low.
  • Always add both twin edges per clause; lit ^ 1 for negation keeps this one line each.

Tests

  • The two fixed examples above (satisfiable with forced x₁, x₂; and x ∧ ¬x → None).
  • SCC: 300 random digraphs (n ≤ 12) vs a reachability-based brute force — same partition, same count, plus the reverse-topo edge property comp[u] > comp[v] for every cross-SCC edge.
  • 2-SAT: 400 random instances (n ≤ 8, up to 3n clauses) vs full 2ⁿ enumeration — satisfiability agrees (307 SAT / 93 UNSAT in the verified run), and every returned assignment is checked clause-by-clause.
  • Scale: a 10⁵-vertex directed cycle → exactly 1 SCC, no recursion error.

Follow-up Questions

  • Tarjan vs Kosaraju — when would you pick each? → Tarjan: one pass, no reversed graph, ids come out in reverse topo order for free. Kosaraju: two simple DFSes, trivial to re-derive when nervous, but needs G-reversed (extra O(n+m) memory) and touches every edge twice. Same asymptotics; in an interview, name both and write the one you’re fluent in.
  • Why does reverse topological order give a valid assignment? → The skew-symmetry chain above: a chosen literal implying a rejected one forces comp[¬l] < comp[¬l]. The intuition: picking the topologically-later SCC means “nothing you imply can escape into a rejected literal,” because implications only move to smaller comp ids.
  • What DP runs on the condensation? → Any DAG DP: longest path where node weight = SCC size (“longest chain of mutually-reachable groups”), reachability counting, min path cover. Process SCCs in comp-id order (already reverse topo) — no separate topo sort needed.
  • Edges arrive online — maintain SCCs incrementally? → Genuinely hard; known incremental algorithms are amortized and complex. Practical answer: offline batching — collect edges, recompute, or divide-and-conquer over the edge timeline. Saying “I’d batch offline” is the right interview move.
  • Why does 3-SAT break this? → (a ∨ b ∨ c) has no binary-implication form: falsifying one literal only yields a disjunction, not an implication edge. That’s the 2→3 cliff — 2-SAT is in P (even NL-complete), 3-SAT is NP-complete. Interviewers probe whether you know the reduction fails structurally, not just “3-SAT is hard.”
  • Where does 2-SAT show up in disguise? → “Each item has two placements, some pairs of placements conflict” — radio frequencies, seating, flag placement on a map, choosing one of two orientations per component.

Product Extension

A feature-flag dependency engine: rules like “flag A requires flag B” (¬A ∨ B) and “A conflicts with B” (¬A ∨ ¬B) are 2-SAT; the solver either emits a valid flag configuration or pinpoints the entangled variable pair (comp[x] == comp[¬x]) as the human-readable conflict. Same machinery: package managers detecting dependency cycles via SCC, and deadlock detectors condensing wait-for graphs.

Language/Runtime Follow-ups

  • Python: iterative only — sys.setrecursionlimit(3*10⁵) still segfaults the C stack on deep chains. Use flat int lists, not dicts; localize adj lookups in the hot loop.
  • C++: recursive Tarjan is fine to ~10⁶ depth with an enlarged stack (or compilers’ default 8 MB handles ~10⁵); most CP code is recursive.
  • Java: default thread stack (~512 KB) dies around 10⁴ frames — the classic fix is running DFS in a new Thread(null, run, "dfs", 1 << 26).
  • Go: goroutine stacks grow dynamically — recursive DFS is safe. Rare and worth knowing.
  • JS/TS: engine call-stack caps near 10⁴ frames; iterative required, same frame-stack pattern.

Common Bugs

  1. Missing on_stk guard: updating low from a vertex in an already-closed SCC (cross edge) merges components that are merely reachable, not mutually reachable. The single most common Tarjan bug.
  2. Re-running the first-visit block: in the iterative form, a frame is visited once per child; without the i == 0 gate, disc is overwritten and the vertex is pushed onto stk repeatedly.
  3. Forgetting the parent low-merge at pop: low[parent] = min(low[parent], low[child]) must happen when the child frame pops — dropping it makes every vertex its own root.
  4. Recursive DFS at scale: RecursionError (or a hard segfault) at 10⁵ nodes in Python; see Language notes.
  5. Wrong 2-SAT edge direction: adding a→b for clause (a ∨ b) instead of ¬a→b, or adding only one twin — breaks skew-symmetry, silently wrong on ~half of random instances.
  6. Flipped assignment comparison: comp[x] < comp[¬x] is correct for Tarjan’s reverse-topo ids; with Kosaraju-ordered ids (forward topo) the inequality flips. Porting code between the two without flipping is a classic silent bug.

Debugging Strategy

Self-check the output first — it’s O(m) and catches everything: for SCC, assert comp[u] ≥ comp[v] for every edge u→v (equality only within a component); for 2-SAT, evaluate every clause under the returned assignment. On failure, shrink with the random tester (n ≤ 5) until minimal, then hand-trace: print (v, disc[v], low[v], stk) at each pop and check against a pencil run of the 5-node graph. If low values look right but components are wrong, the bug is the on_stk guard; if components pop too early, it’s the parent low-merge.

Mastery Criteria

  • Wrote iterative Tarjan from memory, passing the random SCC oracle, in <20 minutes.
  • Wrote the 2-SAT reduction (twin edges + SCC check + assignment) in <10 minutes on top of it.
  • Stated the stack invariant and root condition in <2 minutes without notes.
  • Reproduced the skew-symmetry proof of the assignment rule on a whiteboard.
  • Solved LC 207/210 by explicit condensation framing from cold start.
  • Explained the 2-SAT vs 3-SAT cliff (why implications break at width 3) in <1 minute.