Problem: BOJ 3648 — Idol · 한국어 · 日本語
For each test case, Karl must satisfy all clauses and variable 1 must be true. A clause (a OR b) is represented by the implications ¬a → b and ¬b → a. The required truth of variable 1 is the unit clause (1 OR 1), which adds ¬1 → 1 just like any other clause.
The input contains signed literals. For n variables, the 2n graph vertices are indexed from 0 to 2n - 1: positive literal i maps to i - 1, and negative literal -i maps to n + i - 1. Negation swaps the two halves of this index range. Each implication is stored in both the graph and its reverse graph.
Kosaraju’s algorithm finds strongly connected components using two iterative DFS passes. In the first pass, the stack stores both the current vertex and the index of its next outgoing edge; a vertex is appended to finishing order only after all its edges have been processed. This simulates recursive DFS without using the call stack, so a long implication chain cannot overflow it. The second pass visits the reverse graph in decreasing finishing order and assigns component IDs. The formula is satisfiable exactly when no variable and its negation share a component.
Each case has 2n vertices and 2m + 2 implication edges, including the two edges for (1 OR 1). The algorithm takes O(n + m) time and space per case. Cases are read until EOF, and each answer is printed as lowercase yes or no.
Java
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 input = new BufferedInputStream(System.in);
private final byte[] buffer = new byte[1 << 16];
private int position;
private int length;
private int read() throws IOException {
if (position == length) {
length = input.read(buffer);
position = 0;
if (length == -1) {
return -1;
}
}
return buffer[position++];
}
int nextInt() throws IOException {
int c;
do {
c = read();
} while (c <= ' ' && c != -1);
if (c == -1) {
return Integer.MIN_VALUE;
}
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) {
int variable = Math.abs(literal) - 1;
return literal > 0 ? variable : variable + n;
}
private static int negation(int vertex, int n) {
return vertex < n ? vertex + n : vertex - n;
}
@SuppressWarnings("unchecked")
private static boolean satisfiable(int n, int m, FastScanner input) throws IOException {
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++) {
int a;
int b;
if (i == m) {
a = literalIndex(1, n);
b = a;
} else {
a = literalIndex(input.nextInt(), n);
b = literalIndex(input.nextInt(), 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]) {
return false;
}
}
return true;
}
public static void main(String[] args) throws IOException {
FastScanner input = new FastScanner();
StringBuilder output = new StringBuilder();
while (true) {
int n = input.nextInt();
if (n == Integer.MIN_VALUE) {
break;
}
int m = input.nextInt();
output.append(satisfiable(n, m, input) ? "yes" : "no").append('\n');
}
System.out.print(output);
}
}