BOJ. 2-SAT - 4 (11281)

[Link] https://www.acmicpc.net/problem/11281

Iterative Kosaraju for 2-SAT

Each input clause (a ∨ b) is equivalent to the implications ¬a → b and ¬b → a. Represent every signed literal as a vertex: positive literal x uses index x - 1, and negative literal ¬x uses index N + x - 1. Its negation is the vertex index ^ N. Store every implication in both the graph and its reverse graph.

A formula is unsatisfiable exactly when some variable and its negation belong to the same strongly connected component: each literal then implies the other, forcing both truth values at once. Otherwise, process strongly connected components with Kosaraju’s algorithm. The first pass records finishing order in the original graph; the second pass visits vertices in reverse finishing order in the reversed graph. Both passes below use explicit stacks, so even a long implication chain cannot overflow the Java call stack.

The component IDs are assigned in the order the second pass discovers components. With this traversal order, every edge between distinct components goes from a smaller ID to a larger ID in the original implication graph. Therefore, set variable x to true exactly when component(x) > component(¬x). This is the reverse-topological assignment rule for this particular numbering; reversing the pass order or numbering convention would require reversing the comparison too.

The first pass uses a per-vertex next-edge index to simulate recursive DFS and append a vertex only after all outgoing edges have been explored. The second pass marks each vertex when it is pushed, preventing duplicate stack entries. Each vertex and implication is examined a constant number of times, so the time and space complexities are both O(N + M).

import java.io.BufferedInputStream;
import java.io.IOException;
import java.util.ArrayList;
import java.util.List;

public class Main {
    private static final class FastScanner {
        private final BufferedInputStream in = new BufferedInputStream(System.in);
        private final byte[] buffer = new byte[1 << 16];
        private int pointer;
        private int length;

        private int read() throws IOException {
            if (pointer == length) {
                length = in.read(buffer);
                pointer = 0;
                if (length == -1) {
                    return -1;
                }
            }
            return buffer[pointer++];
        }

        int nextInt() throws IOException {
            int c;
            do {
                c = read();
            } while (c <= ' ' && c != -1);

            int sign = 1;
            if (c == '-') {
                sign = -1;
                c = read();
            }

            int value = 0;
            while (c > ' ') {
                value = value * 10 + c - '0';
                c = read();
            }
            return value * sign;
        }
    }

    private static int literalIndex(int literal, int n) {
        return literal > 0 ? literal - 1 : n - literal - 1;
    }

    public static void main(String[] args) throws Exception {
        FastScanner input = new FastScanner();
        int n = input.nextInt();
        int m = input.nextInt();
        int vertexCount = 2 * n;

        List<Integer>[] graph = new ArrayList[vertexCount];
        List<Integer>[] reverseGraph = new ArrayList[vertexCount];
        for (int vertex = 0; vertex < vertexCount; vertex++) {
            graph[vertex] = new ArrayList<>();
            reverseGraph[vertex] = new ArrayList<>();
        }

        for (int clause = 0; clause < m; clause++) {
            int a = input.nextInt();
            int b = input.nextInt();
            int notA = literalIndex(-a, n);
            int indexA = literalIndex(a, n);
            int notB = literalIndex(-b, n);
            int indexB = literalIndex(b, n);

            graph[notA].add(indexB);
            reverseGraph[indexB].add(notA);
            graph[notB].add(indexA);
            reverseGraph[indexA].add(notB);
        }

        boolean[] visited = new boolean[vertexCount];
        int[] nextEdge = new int[vertexCount];
        int[] stack = new int[vertexCount];
        int[] order = new int[vertexCount];
        int orderSize = 0;

        for (int start = 0; start < vertexCount; start++) {
            if (visited[start]) {
                continue;
            }
            int top = 0;
            stack[top++] = start;
            visited[start] = true;

            while (top > 0) {
                int vertex = stack[top - 1];
                if (nextEdge[vertex] < graph[vertex].size()) {
                    int next = graph[vertex].get(nextEdge[vertex]++);
                    if (!visited[next]) {
                        visited[next] = true;
                        stack[top++] = next;
                    }
                } else {
                    order[orderSize++] = vertex;
                    top--;
                }
            }
        }

        int[] component = new int[vertexCount];
        int componentCount = 0;
        for (int index = orderSize - 1; index >= 0; index--) {
            int start = order[index];
            if (component[start] != 0) {
                continue;
            }
            int top = 0;
            stack[top++] = start;
            component[start] = ++componentCount;

            while (top > 0) {
                int vertex = stack[--top];
                for (int next : reverseGraph[vertex]) {
                    if (component[next] == 0) {
                        component[next] = componentCount;
                        stack[top++] = next;
                    }
                }
            }
        }

        for (int variable = 0; variable < n; variable++) {
            if (component[variable] == component[variable + n]) {
                System.out.println(0);
                return;
            }
        }

        StringBuilder output = new StringBuilder("1\n");
        for (int variable = 0; variable < n; variable++) {
            output.append(component[variable] > component[variable + n] ? '1' : '0');
            if (variable + 1 < n) {
                output.append(' ');
            }
        }
        output.append('\n');
        System.out.print(output);
    }
}