강연결 요소와 2-SAT — 그래프의 구조를 분석하는 법

예: A → B → C → A (하나의 SCC)
    D → E (D에서 E는 가지만, E에서 D로는 못 감 → 같은 SCC 아님)

public class Kosaraju {
    private int n;
    private List<List<Integer>> graph;    // 원래 그래프
    private List<List<Integer>> reversed; // 역전 그래프
    private boolean[] visited;
    private Deque<Integer> finishOrder;   // 종료 순서 스택

    public List<List<Integer>> findSCCs(List<List<Integer>> graph, int n) {
        this.n = n;
        this.graph = graph;
        this.reversed = new ArrayList<>();
        this.visited = new boolean[n];
        this.finishOrder = new ArrayDeque<>();

        // 역전 그래프 구성
        for (int i = 0; i < n; i++) reversed.add(new ArrayList<>());
        for (int u = 0; u < n; u++) {
            for (int v : graph.get(u)) {
                reversed.get(v).add(u);
            }
        }

        // 1단계: 원래 그래프에서 DFS, 종료 순서 기록
        for (int i = 0; i < n; i++) {
            if (!visited[i]) dfs1(i);
        }

        // 2단계: 역전 그래프에서 종료 역순으로 DFS
        Arrays.fill(visited, false);
        List<List<Integer>> sccs = new ArrayList<>();

        while (!finishOrder.isEmpty()) {
            int node = finishOrder.pop();
            if (!visited[node]) {
                List<Integer> scc = new ArrayList<>();
                dfs2(node, scc);
                sccs.add(scc);
            }
        }
        return sccs;
    }

    private void dfs1(int u) {
        visited[u] = true;
        for (int v : graph.get(u)) {
            if (!visited[v]) dfs1(v);
        }
        finishOrder.push(u); // 종료 시점에 스택에 추가
    }

    private void dfs2(int u, List<Integer> scc) {
        visited[u] = true;
        scc.add(u);
        for (int v : reversed.get(u)) {
            if (!visited[v]) dfs2(v, scc);
        }
    }
}

public class Tarjan {
    private int n, timer;
    private int[] disc, low;
    private boolean[] onStack;
    private Deque<Integer> stack;
    private List<List<Integer>> graph;
    private List<List<Integer>> sccs;

    public List<List<Integer>> findSCCs(List<List<Integer>> graph, int n) {
        this.n = n;
        this.graph = graph;
        this.timer = 0;
        this.disc = new int[n];
        this.low = new int[n];
        this.onStack = new boolean[n];
        this.stack = new ArrayDeque<>();
        this.sccs = new ArrayList<>();
        Arrays.fill(disc, -1);

        for (int i = 0; i < n; i++) {
            if (disc[i] == -1) dfs(i);
        }
        return sccs;
    }

    private void dfs(int u) {
        disc[u] = low[u] = timer++;
        stack.push(u);
        onStack[u] = true;

        for (int v : graph.get(u)) {
            if (disc[v] == -1) {
                dfs(v);
                low[u] = Math.min(low[u], low[v]);
            } else if (onStack[v]) {
                low[u] = Math.min(low[u], disc[v]);
            }
        }

        // u가 SCC의 루트인 경우
        if (low[u] == disc[u]) {
            List<Integer> scc = new ArrayList<>();
            while (true) {
                int v = stack.pop();
                onStack[v] = false;
                scc.add(v);
                if (v == u) break;
            }
            sccs.add(scc);
        }
    }
}

// SCC 축약 후 DAG 구성
int[] sccId = new int[n]; // 각 정점이 속한 SCC 번호
// ... SCC 찾기 과정에서 sccId 설정 ...

Set<Long> dagEdges = new HashSet<>();
List<List<Integer>> dag = new ArrayList<>();
for (int i = 0; i < sccCount; i++) dag.add(new ArrayList<>());

for (int u = 0; u < n; u++) {
    for (int v : graph.get(u)) {
        if (sccId[u] != sccId[v]) {
            long key = (long) sccId[u] * n + sccId[v];
            if (dagEdges.add(key)) {
                dag.get(sccId[u]).add(sccId[v]);
            }
        }
    }
}
// 이제 dag에 위상 정렬 등을 적용할 수 있습니다

(x₁ ∨ x₂) → (¬x₁ → x₂) ∧ (¬x₂ → x₁)