DSA DSA In Depth
0%
From-Scratch Build

Tarjan Strongly Connected Components & Linear-Time 2-SAT Solver

Tarjan single-pass low-link Strongly Connected Components (SCC) engine and a linear-time 2-SAT boolean satisfiability solver over implication graphs.

~45 min Advanced Lessons: Build Lab: Tarjan's SCC Condensation DAG & Linear-Time 2-SAT Constraint Solver, Strongly Connected Components: Kosaraju's Two-Pass vs Tarjan's Single-Pass Stack & 2-SAT, Depth-First Search: Parenthesis Theorem, White-Path Theorem & Tree/Back/Forward/Cross Edges, Directed Acyclic Graphs (DAGs): Kahn's Indegree Queue vs DFS Post-Order Reversal, Undirected Connectivity: Tarjan's tin/low Algorithm for Bridges, Cut Vertices & BCCs, Branch and Bound: Best-First / DFS Relaxation Bounds for Combinatorial Optimization
Interactive Build Lab 0/4 Steps Completed

Code & Verify in the Browser Workbench

Complete 4 progressive engineering steps in JavaScript or TypeScript against an in-browser Node.js v22 runtime (virtual filesystem, loopback TCP/HTTP, and automated unit tests) — zero local setup required.

Tarjan's Single-Pass Low-Link Algorithm

Robert Tarjan (1972) showed that Strongly Connected Components (SCCs) can be extracted in a single DFS pass by maintaining two integers per vertex $u$:

  • $\text{disc}[u]$: the timestamp when $u$ is first visited.
  • $\text{low}[u]$: the smallest $\text{disc}$ reachable from $u$'s DFS subtree using at most one back/cross edge to a vertex still on the active SCC stack.

A vertex $u$ is the root of its SCC if and only if $\text{low}[u] = \text{disc}[u]$ after exploring all outgoing edges. Moreover, because children SCCs finish before their parents, Tarjan's algorithm naturally outputs SCCs in reverse topological order.

Reducing 2-SAT to SCC in $O(V + E)$ Time

While 3-SAT is NP-complete, 2-SAT ($\bigwedge_k (a_k \lor b_k)$) is solvable in linear time:

  1. Rewrite each clause $(a \lor b)$ as two logically equivalent implications: $(\lnot a \Rightarrow b)$ and $(\lnot b \Rightarrow a)$.
  2. Decompose the $2n$-vertex implication graph into SCCs using Tarjan's algorithm.
  3. If any variable $x_i$ and its negation $\lnot x_i$ belong to the same SCC ($x_i \Leftrightarrow \lnot x_i$), the formula is unsatisfiable.
  4. Otherwise, choosing whichever literal appears later in topological order (smaller Tarjan compId) never triggers a true-implies-false edge, yielding a valid truth assignment in $O(V + E)$ time.

Curriculum Connections

Guided Implementation Walkthrough (4 Progressive Steps)

Step 1: Discovery & Low-Link Invariant Maintenance

  • Core Mechanical Concept: Discovery & Low-Link Invariant Maintenance
  • Target Module: index.js (Step1)
  • Engineering Specification: In tarjanSCC, track disc[u] and low[u]. On tree edges update low[u] = Math.min(low[u], low[v]); on back/cross edges to vertices currently onStack update low[u] = Math.min(low[u], disc[v]).
  • Verification Invariant: verifies Step 1: Discovery & Low-Link Invariant Maintenance

Step 2: SCC Root Identification & Stack Popping

  • Core Mechanical Concept: SCC Root Identification & Stack Popping
  • Target Module: index.js (Step2)
  • Engineering Specification: When low[u] === disc[u], u is the entry root of an SCC. Pop vertices from the active stack until u is popped; notice that components are emitted in reverse topological order.
  • Verification Invariant: verifies Step 2: SCC Root Identification & Stack Popping

Step 3: 2-SAT Implication Graph Construction

  • Core Mechanical Concept: 2-SAT Implication Graph Construction
  • Target Module: index.js (Step3)
  • Engineering Specification: Encode boolean variable $x_i$ as vertex $2i$ and $\lnot x_i$ as $2i+1$ (so negation is node ^ 1). Every clause $(A \lor B)$ adds directed edges $(\lnot A \to B)$ and $(\lnot B \to A)$.
  • Verification Invariant: verifies Step 3: 2-SAT Implication Graph Construction

Step 4: Linear-Time Satisfiability & Truth Assignment

  • Core Mechanical Concept: Linear-Time Satisfiability & Truth Assignment
  • Target Module: index.js (Step4)
  • Engineering Specification: Run tarjanSCC on the $2n$-vertex implication graph. The formula is satisfiable iff compId[2*i] !== compId[2*i+1] for all $i$, with assignment[i] = compId[2*i] < compId[2*i+1].
  • Verification Invariant: verifies Step 4: Linear-Time Satisfiability & Truth Assignment

Asymptotic & Memory Layout Guarantees

  • Category: Graph Algorithms
  • Difficulty: Advanced (~45 minutes)
  • Key Architectural Highlights:
    • Single-pass Tarjan DFS computing discovery times, low-link values, and reverse-topological SCC IDs
    • Implication graph encoding (a v b) as (~a -> b) and (~b -> a) over 2n literal vertices
    • Linear-time O(V + E) 2-SAT satisfiability check and truth assignment extraction
  • Tags & Primitives: Tarjan SCC, Low-Link Invariant, Condensation DAG, 2-SAT Solver, Implication Graph

Production Systems Context & Verification

This from-scratch implementation is engineered with zero external dependencies and deterministic verification harnesses. Every internal invariant—from pointer restoration and bitmask addressing to amortized potential bounds and tree height balance—is asserted directly in test.js. Use the interactive browser workbench above to complete the guided steps in Guided Lab mode or inspect and benchmark the complete reference architecture in Full Solution mode.