Strongly Connected Components: Kosaraju's Two-Pass vs Tarjan's Single-Pass Stack & 2-SAT

SCC Equivalence Classes & The Condensation DAG

Given $G = (V, E)$, define $u \sim v \iff (u \leadsto v \land v \leadsto u)$. The equivalence classes $C_1, C_2, \dots, C_k$ are the Strongly Connected Components of $G$. The condensation graph $G^{\text{SCC}} = (V^{\text{SCC}}, E^{\text{SCC}})$ has a vertex for each $C_i$ and a directed edge $(C_i, C_j)$ whenever there is some $u \in C_i, v \in C_j$ with $(u, v) \in E$ ($i \neq j$). By construction, $G^{\text{SCC}}$ is guaranteed to be a DAG.

1. Kosaraju's Two-Pass Algorithm vs. Tarjan's Single-Pass Algorithm

• Kosaraju-Sharir (Two DFS Passes + Graph Transpose): Pass 1 runs DFS on $G$ and records vertices in decreasing order of finish time $\text{tout}[u]$. Since the SCC with the global maximum $\text{tout}$ is a source in $G^{\text{SCC}}$, it is a sink in the transposed graph $G^T$ (all edges reversed). Pass 2 runs DFS on $G^T$ in that order; each DFS tree in $G^T$ is trapped inside a single sink SCC and peels components in topological order.
• Tarjan's Algorithm (Single DFS Pass, Zero Transpose): Avoids constructing $G^T$ (saving $O(E)$ memory and half the cache misses). Because Tarjan emits each SCC when its root finishes post-order, component IDs $0, 1, \dots, k-1$ are emitted in reverse topological order (sinks of $G^{\text{SCC}}$ first, sources last).

2. Linear-Time 2-SAT via Implication Graph SCCs

While 3-SAT is NP-complete, 2-SAT (a conjunction of clauses $(a \lor b)$ with two literals per clause) is solvable in $O(V + E)$ linear time (Aspvall, Plass & Tarjan, 1979). Rewrite each clause $(a \lor b)$ as two contrapositive logical implications:

Construct a directed implication graph with $2n$ vertices ($2i$ for $x_i$ and $2i+1$ for $\neg x_i$):

• Satisfiability Theorem: The 2-SAT formula is satisfiable if and only if no variable $x_i$ belongs to the same SCC as its negation $\neg x_i$ ($\text{comp}[2i] \neq \text{comp}[2i+1]$).
• Truth Assignment: Because $p \Rightarrow q$ means True cannot imply False, if $x_i$ is reachable from $\neg x_i$, then $x_i$ appears in an SCC that is topologically later (closer to a sink, hence smaller Tarjan component ID) than $\neg x_i$. Setting $x_i = (\text{comp}[2i] < \text{comp}[2i+1])$ always produces a valid satisfying assignment!

Complexity Matrix

Production Implementation: Tarjan's SCC & 2-SAT Solver

#include <vector>
#include <algorithm>

struct TarjanSCC {
    int n, timer = 0, numComponents = 0;
    std::vector<std::vector<int>> adj;
    std::vector<int> tin, low, comp, st;
    std::vector<uint8_t> onStack;

    explicit TarjanSCC(int vertices)
        : n(vertices), adj(vertices), tin(vertices, 0),
          low(vertices, 0), comp(vertices, -1), onStack(vertices, 0) {
        st.reserve(vertices);
    }

    void addEdge(int u, int v) { adj[u].push_back(v); }

    void dfs(int u) {
        tin[u] = low[u] = ++timer;
        st.push_back(u);
        onStack[u] = 1;

        for (int v : adj[u]) {
            if (tin[v] == 0) {
                dfs(v);
                low[u] = std::min(low[u], low[v]);
            } else if (onStack[v]) {
                low[u] = std::min(low[u], tin[v]);
            }
        }

        if (low[u] == tin[u]) {
            while (true) {
                int w = st.back();
                st.pop_back();
                onStack[w] = 0;
                comp[w] = numComponents;
                if (w == u) break;
            }
            ++numComponents;
        }
    }

    void solve() {
        for (int i = 0; i < n; ++i) {
            if (tin[i] == 0) dfs(i);
        }
    }
};