문제: BOJ 3648 — 아이돌 · English · 日本語
각 테스트 케이스에서 모든 절을 만족시키고 변수 1을 참으로 만들어야 합니다. 절 (a OR b)는 함의 ¬a → b, ¬b → a라는 두 간선으로 바꿉니다. 변수 1을 참으로 만드는 조건은 단위 절 (1 OR 1)로 추가하며, 다른 절과 마찬가지로 ¬1 → 1 간선을 생성합니다.
입력 리터럴은 부호가 있는 정수입니다. 변수 n개에 대해 그래프 정점은 2n개이며 인덱스 범위는 0부터 2n - 1까지입니다. 양수 리터럴 i는 i - 1, 음수 리터럴 -i는 n + i - 1로 매핑합니다. 부정은 이 두 인덱스 영역을 서로 바꿉니다. 각 함의 간선은 정방향 그래프와 역방향 그래프에 함께 저장합니다.
강한 연결 요소(SCC)는 반복문과 명시적 스택을 사용하는 코사라주 알고리즘으로 구합니다. 첫 번째 순회에서는 스택에 현재 정점뿐 아니라 다음에 방문할 간선의 위치도 저장합니다. 모든 간선을 처리한 뒤에야 정점을 종료 순서에 추가해 재귀 DFS의 동작을 정확히 재현합니다. 따라서 간선이 긴 사슬을 이루어도 호출 스택이 넘치지 않습니다. 두 번째 순회는 종료 순서의 역순으로 역방향 그래프를 방문해 SCC 번호를 붙입니다. 변수와 그 부정 리터럴이 같은 SCC에 속하는 변수가 하나라도 있으면 만족 불가능합니다.
각 케이스의 정점은 2n개, 함의 간선은 (1 OR 1)을 포함해 2m + 2개입니다. 시간 및 공간 복잡도는 케이스마다 O(n + m)입니다. 입력은 EOF까지 읽으며 각 케이스마다 소문자 yes 또는 no를 출력합니다.
Java
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
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);
}
}