BOJ. 2-SAT - 3 (11280)

Problem: BOJ 11280 — 2-SAT - 3 · 한국어 · 日本語

Each clause (a OR b) becomes two implications: ¬a → b and ¬b → a. The input literals are signed integers. Encode the positive literal for variable i (i) as vertex i - 1, and the negative literal (-i) as vertex N + i - 1. Thus, the negation of a vertex v is v + N when v < N, and v - N otherwise. Store every implication in both the forward graph and its reverse.

Find strongly connected components (SCCs) with iterative Kosaraju. The first pass uses an explicit stack that also stores each vertex’s next edge position, producing DFS finishing order without recursion. Processing the vertices in reverse finishing order on the reverse graph assigns component IDs. If a variable and its negation belong to the same SCC, each implies the other, forcing both to be true; the formula is contradictory. Otherwise it is satisfiable. Unit clauses need no special handling: (x OR x), for example, adds the implication ¬x → x.

There are 2N vertices and 2M implication edges. Both graph passes take O(N + M) time and space. Print only 1 if the formula is satisfiable, or 0 otherwise.

Java

import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.List;
import java.util.StringTokenizer;

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

    private static int negation(int vertex, int n) {
        return vertex < n ? vertex + n : vertex - n;
    }

    public static void main(String[] args) throws IOException {
        BufferedReader input = new BufferedReader(new InputStreamReader(System.in));
        StringTokenizer first = new StringTokenizer(input.readLine());
        int n = Integer.parseInt(first.nextToken());
        int m = Integer.parseInt(first.nextToken());
        int vertices = 2 * n;

        List<Integer>[] graph = new ArrayList[vertices];
        List<Integer>[] reverse = new ArrayList[vertices];
        for (int v = 0; v < vertices; v++) {
            graph[v] = new ArrayList<>();
            reverse[v] = new ArrayList<>();
        }

        for (int i = 0; i < m; i++) {
            StringTokenizer clause = new StringTokenizer(input.readLine());
            int a = literalIndex(Integer.parseInt(clause.nextToken()), n);
            int b = literalIndex(Integer.parseInt(clause.nextToken()), n);
            int notA = negation(a, n);
            int notB = negation(b, n);
            graph[notA].add(b);
            reverse[b].add(notA);
            graph[notB].add(a);
            reverse[a].add(notB);
        }

        boolean[] visited = new boolean[vertices];
        int[] order = new int[vertices];
        int orderSize = 0;
        int[] stackVertex = new int[vertices];
        int[] stackNext = new int[vertices];

        for (int start = 0; start < vertices; start++) {
            if (visited[start]) {
                continue;
            }
            int top = 0;
            stackVertex[top] = start;
            stackNext[top] = 0;
            visited[start] = true;
            while (top >= 0) {
                int v = stackVertex[top];
                if (stackNext[top] < graph[v].size()) {
                    int next = graph[v].get(stackNext[top]++);
                    if (!visited[next]) {
                        visited[next] = true;
                        stackVertex[++top] = next;
                        stackNext[top] = 0;
                    }
                } else {
                    order[orderSize++] = v;
                    top--;
                }
            }
        }

        int[] component = new int[vertices];
        int componentId = 0;
        int[] stack = new int[vertices];
        for (int i = orderSize - 1; i >= 0; i--) {
            int start = order[i];
            if (component[start] != 0) {
                continue;
            }
            componentId++;
            int top = 0;
            stack[top++] = start;
            component[start] = componentId;
            while (top > 0) {
                int v = stack[--top];
                for (int next : reverse[v]) {
                    if (component[next] == 0) {
                        component[next] = componentId;
                        stack[top++] = next;
                    }
                }
            }
        }

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