Skip to content

Strong Connectivity & 2SAT

A directed graph is strongly connected if every vertex can reach every other vertex. SCCs (strongly connected components) partition the graph into maximal such subgraphs.

Kosaraju (two-pass DFS)

  1. DFS on G, push vertices to a stack by finish time.
  2. DFS on transposed graph G^T (edges reversed), processing vertices in stack order; each DFS tree is one SCC.
#include <vector>
#include <algorithm>
using namespace std;

void dfsOrder(int u, const vector<vector<int>>& adj, vector<bool>& vis, vector<int>& order) {
    vis[u] = true;
    for (int v : adj[u])
        if (!vis[v]) dfsOrder(v, adj, vis, order);
    order.push_back(u);
}

void dfsComp(int u, const vector<vector<int>>& radj, vector<bool>& vis, vector<int>& comp, int id) {
    vis[u] = true;
    comp[u] = id;
    for (int v : radj[u])
        if (!vis[v]) dfsComp(v, radj, vis, comp, id);
}

// Returns component id per vertex (0..numComp-1)
vector<int> kosaraju(const vector<vector<int>>& adj) {
    int n = (int)adj.size();
    vector<int> order;
    vector<bool> vis(n, false);
    for (int i = 0; i < n; i++)
        if (!vis[i]) dfsOrder(i, adj, vis, order);
    reverse(order.begin(), order.end());

    vector<vector<int>> radj(n);
    for (int u = 0; u < n; u++)
        for (int v : adj[u]) radj[v].push_back(u);

    fill(vis.begin(), vis.end(), false);
    vector<int> comp(n, -1);
    int cid = 0;
    for (int u : order)
        if (!vis[u]) {
            dfsComp(u, radj, vis, comp, cid);
            cid++;
        }
    return comp;
}

2SAT

Variables \(x_0,\ldots,x_{n-1}\) boolean. Clauses \((a \lor b)\) where each literal is \(x_i\) or \(\neg x_i\).

Build implication graph: \(2n\) vertices (for each \(x_i\), vertices 2*i and 2*i+1 for true/false). Clause \((a \lor b)\) adds edges \(\neg a \to b\) and \(\neg b \to a\).

Satisfiable iff no variable and its negation lie in the same SCC. Assign truth by topological order of SCC condensation (or order of Kosaraju’s second pass).