Strong Connectivity

Kosaraju’s Algorithm

This is a template to solve 2SAT.

2-SAT

2SAT (Boolean satisfiability problem) is the problem of assigning Boolean values to variables to satisfy a given Boolean formula.

$(x_1\vee x_2)\wedge (x_3\vee x_4)\vee \dots$

The original 2-sat logic: You convert the or statements into a series of implications, great video by Algorithms live to rewatch here.

For solving 2SAT, you just follow 2 simple steps:

1. Translate the problem in the right variables
2. Apply the 2SAT algorithm

The choice of the variables is very important.

comp[v] (comp == component) denotes the index of strongly connected component to which the vertex belongs.

int n;
vector<vector<int>> adj, adj_t;
vector<bool> used;
vector<int> order, comp;
vector<bool> assignment;
 
void dfs1(int v) {
    used[v] = true;
    for (int u : adj[v]) {
        if (!used[u])
            dfs1(u);
    }
    order.push_back(v);
}
 
void dfs2(int v, int cl) {
    comp[v] = cl;
    for (int u : adj_t[v]) {
        if (comp[u] == -1)
            dfs2(u, cl);
    }
}
 
bool solve_2SAT() {
    order.clear();
    used.assign(n, false);
 
    // Search 1: Create Reverse Topological Order
    for (int i = 0; i < n; ++i) {
        if (!used[i])
            dfs1(i);
    }
 
    comp.assign(n, -1);
 
    // Search 2: Go through list of nodes in the reverse of the reverse topological order?? 
    for (int i = 0, j = 0; i < n; ++i) {
        int v = order[n - i - 1];
        if (comp[v] == -1)
            dfs2(v, j++);
    }
 
    // Solve the 2SAT Problem
    assignment.assign(n / 2, false);
    for (int i = 0; i < n; i += 2) {
        if (comp[i] == comp[i + 1])
            return false;
        assignment[i / 2] = comp[i] > comp[i + 1];
    }
    return true;
}
 
void add_disjunction(int a, bool na, int b, bool nb) {
    // na and nb signify whether a and b are to be negated 
    a = 2*a ^ na;
    b = 2*b ^ nb;
    int neg_a = a ^ 1;
    int neg_b = b ^ 1;
    adj[neg_a].push_back(b);
    adj[neg_b].push_back(a);
    adj_t[b].push_back(neg_a);
    adj_t[a].push_back(neg_b);
}

Finding strongly-connected component

Learned this from CS341. There are 3 simple steps

1. Run DFS on G, store the finish time of each vertex
2. Run DFS on G^T, starting with vertices with highest finish time
3. Each tree in the DFS forest we get from step 2 is a strongly connected component.

Step 2 essentially proceeds like a topological order.