문제 49
2-SAT
$N$개의 불 변수 $x_1, x_2, \cdots, x_N$이 있다.
각 변수에는 true 또는 false를 할당할 수 있다.
$M$개의 조건이 주어진다.
양의 정수 $k$는 $x_k$, 음의 정수 $-k$는 $\lnot x_k$를 의미한다.
각 조건은 두 리터럴 중 하나 이상이 true여야 한다.
모든 조건을 만족하도록 변수의 값을 정할 수 있는지 판별하라.
입력
첫 번째 줄에 두 정수 $N$, $M$이 공백으로 구분되어 주어진다. $(1 \le N \le 10\,000; 0 \le M \le 100\,000)$
두 번째 줄부터 $M$개의 줄에 걸쳐 각 조건의 두 리터럴을 의미하는 두 정수 $a$, $b$가 공백으로 구분되어 주어진다. $(-N \le a, b \le N; a \neq 0; b \neq 0)$
출력
모든 조건을 만족하도록 변수의 값을 정할 수 있다면 Yes를, 그렇지 않다면 No를 출력한다.
예제 입력 1
3 4 1 2 -1 3 -2 3 -3 1
예제 출력 1
Yes
예제 입력 2
1 2 1 1 -1 -1
예제 출력 2
No
공식 해설
변수가 최대 $10\,000$개이므로 모든 참·거짓 배정을 열거할 수는 없다. 각 조건이 두 리터럴의 논리합이라는 점을 이용해, 한 값이 다른 값을 강제하는 관계로 바꾼다.
조건을 함의로 바꾸기
조건 $a\lor b$는 둘 중 하나 이상이 참이어야 한다는 뜻이다. 이는 두 함의 $\lnot a\Rightarrow b$, $\lnot b\Rightarrow a$와 동치이다.
각 변수와 그 부정을 별도 정점으로 만들고, 조건마다 위 두 방향 간선을 추가한다. 그래프에서 경로가 있으면 시작 리터럴이 참일 때 도착 리터럴도 참이어야 한다.
어떤 $x_i$와 $\lnot x_i$가 같은 강한 연결 요소(SCC)에 있으면 서로를 참으로 강제한다. 어느 쪽을 참으로 정해도 모순이므로 이 경우에는 No이다.
같은 SCC에만 없으면 충분한 이유
모든 변수와 부정이 서로 다른 SCC에 있다고 하자. SCC들을 위상 순서로 나열하고, 각 변수에서 더 뒤에 있는 리터럴을 참으로 정한다.
이 배정이 $a\Rightarrow b$를 어긴다면 $a$는 참이고 $b$는 거짓이다. SCC의 위상 순서를 $t$라 하면 $t(\lnot a)<t(a)$, $t(b)<t(\lnot b)$이다. 함의의 대우인 $\lnot b\Rightarrow\lnot a$도 그래프에 있으므로
\[
t(\lnot a)<t(a)\le t(b)<t(\lnot b)\le t(\lnot a)
\]
가 되어 모순이다. 따라서 위 배정은 모든 조건을 만족한다.
실제로 배정할 필요는 없으므로 SCC를 구한 뒤 각 변수와 부정의 번호가 다른지만 확인한다. 정점 $2N$개와 간선 $2M$개를 처리하므로 시간복잡도와 공간복잡도는 $O(N+M)$이다.
구현 · 언어별 풀이
C++ 구현
변수 $i$와 그 부정을 인덱스 2 * i, 2 * i + 1로 대응시키면 반대 리터럴은 v ^ 1로 구할 수 있다. 조건 $a\lor b$마다 반대 $a$에서 $b$, 반대 $b$에서 $a$로 간선을 넣는다. SCC 번호를 얻으면 각 변수의 두 번호가 같은지만 확인한다.
C 구현
변수마다 참·거짓 두 정점을 만들고 반대 리터럴을 xor 1로 구한다. 각 절에서 두 함의 간선을 추가한 뒤 SCC를 계산한다. 성분 번호 int 배열에서 같은 변수의 두 정점이 같은지 검사한다.
Python 구현
2*N 정점의 함의 그래프와 역그래프를 만들고 반복 DFS로 SCC를 구한다. 리터럴을 0-based 쌍에 대응시키면 부정은 xor 1이다. 참값 배정을 만들 필요 없이 성분 충돌만 확인한다.
Java 구현
리터럴 번호를 int로 변환하고 부정은 번호 ^ 1로 계산한다. SCC 탐색은 명시적 스택으로 작성해 긴 함의 경로에서도 스택 오버플로를 피한다. 두 리터럴의 성분 번호만 비교하면 된다.
Rust 구현
입력은 i32로 읽고 부호를 확인한 뒤 0-based usize 정점으로 바꾼다. 부정은 xor 1로 구한다. 반복 DFS로 SCC를 계산하고 각 변수의 두 성분을 비교한다.
JavaScript 구현
리터럴을 $0$부터 $2N-1$까지의 정점으로 바꾸고, 한 변수의 양수·음수 리터럴은 연속된 두 번호로 둔다. 그러면 부정은 v ^ 1로 얻는다. 각 절에서 만드는 두 간선을 원래 그래프와 역방향 그래프에 함께 저장한다.
Kosaraju의 첫 순회는 정점과 다음에 확인할 간선 위치를 담은 스택으로 끝나는 순서를 기록한다. 두 번째 순회는 역방향 그래프에서 단순 스택으로 SCC 번호를 매긴다. 재귀 DFS는 $20\,000$개 정점이 이어진 입력에서 Node.js 호출 스택을 넘을 수 있다.
마지막에는 모든 변수의 두 리터럴이 같은 SCC인지 비교한다. 가능한지만 묻는 문제이므로 실제 참·거짓 배정 배열은 만들지 않는다. 정점 번호와 SCC 번호는 Int32Array에 저장할 수 있고, 시간·공간복잡도는 공통 풀이의 $O(N+M)$이다.