問題: BOJ 3648 — アイドル · English · 한국어
各テストケースでは、すべての節を満たし、変数 1 を真にする必要があります。節 (a OR b) は、含意 ¬a → b と ¬b → a の2本の辺に変換します。変数 1 を真にする条件は単位節 (1 OR 1) として追加し、他の節と同じように ¬1 → 1 の辺を作ります。
入力リテラルは符号付き整数です。変数が n 個の場合、グラフの頂点数は 2n で、インデックスは 0 から 2n - 1 です。正リテラル i は i - 1、負リテラル -i は n + i - 1 に対応します。否定を取ると、この2つのインデックス領域が入れ替わります。各含意辺は順方向グラフと逆方向グラフの両方に保存します。
強連結成分（SCC）は、明示的なスタックを使う反復型コサラジュ法で求めます。1回目の探索では、現在の頂点と次に調べる辺の位置をスタックに保持します。すべての辺を処理した後に頂点を終了順に追加することで、再帰DFSと同じ順序を得ます。したがって、含意辺が長い鎖を作っても呼び出しスタックはあふれません。2回目は終了順の逆順に逆方向グラフを探索して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);
}
}