2-SAT 및 그의 응용
1. 2-SAT 문제란?
2-SAT 문제란 참/거짓의 값을 가지는 불리언 변수 $n$개 $x_1, x_2, \cdots, x_n$ 와 2-CNF가 있을 때, 2-CNF를 참으로 만들기 위해 $x_i$ 들에 적당한 값을 할당하는 문제이다. 2-CNF란 2개의 변수를 $\lor$ (or)한 식(절) 여러 개에 $\land$ 연산을 취해 만들어지는 식을 의미한다.
예를 들어, $(x_1 \lor x_2) \land (\bar x_3 \lor x_4)$ 는 2-CNF이다. 그리고, $x_1 = true$, $x_2 = false$, $x_3 = false$, $x_4 = false$ 는 이 식을 만족 시키는 하나의 방법이다. 반대로, $(x_1 \lor x_1) \land (\bar x_1 \lor \bar x_1)$ 의 경우, $x_1$에 어떤 값을 할당하더라도 식을 만족시킬 수 없다. (단, $\bar p$는 $p$의 부정을 나타낸다.)
2. 2-SAT 문제를 해결하는 방법
이 섹션에서는 SCC를 구하는 방법을 안다고 가정하고 설명을 진행한다.
두 불리언 변수 $p$에 대해 $p \to q$ 와 $\bar p \lor q$는 동치임은 진리표를 그려 보면 쉽게 알 수 있다. 그렇다면, 반대로 $p \lor q$ 는 $\bar p \to q$, $\bar q \to p$ 와 동치임을 알 수 있다.
그래서 우리는 $2n$개의 정점 $x_1, \bar x_1, x_2, \bar x_2, \cdots, x_n, \bar x_n$과 각 clause $p \lor q$에 대해 $\bar p \to q$, $\bar q \to p$ 의 간선을 추가한 그래프를 만들 것이다. 이 그래프에서, $x_i, \bar x_i$의 관계를 생각해보면 다음 세 가지 중 하나이다.
- $x_i \to \bar x_i$ 경로와 $\bar x_i \to x_i$ 경로가 모두 존재한다.
- $x_i \to \bar x_i$ 경로와 $\bar x_i \to x_i$ 경로 중 하나만 존재한다.
- $x_i, \bar x_i$ 사이에 어느 방향의 경로도 존재하지 않는다.
위 세 경우에 대해 생각해보면,
- 이 경우에는 $x_i \to \bar x_i$ 이고, $x_i \leftarrow \bar x_i$ 라 $x_i \Leftrightarrow \bar x_i$ 가 되고, 이는 모순이다. 고로, 이러한 경우가 존재하면, 충족 가능하지 않다.
- 이 두 경로 중 하나만 존재한다면, “가정이 거짓인 명제는 항상 참”이기 때문에, “결론 부분에 오는 정점”, 즉, 위상정렬 순서가 더 늦은 쪽이 참이 된다.
- 이 경우는 딱히 고려할게 없어서 해피한 경우다.
따라서, 다음의 과정을 통해 2-SAT 문제를 풀 수 있다:
- 2-CNF 식으로 부터 그래프를 구성한다. (참고로, 이 그래프는 implication graph라 부른다.)
- SCC로 그래프를 분해한다.
- $x_i, \bar x_i$ 가 같은 SCC에 속하는 경우가 있으면, unsatisfiable이라 결론 내린다.
- 그렇지 않다면, 각 $x_i, \bar x_i$ 에 대해 이 둘의 위상 정렬 순서를 비교해보고 참/거짓을 결정해준다.
3. 2-SAT의 응용
2-SAT 자체의 구현은 SCC만 구현할 수 있으면 어려울게 없다. 더 중요한 것은, 실제 세계의 문제 혹은 대회의 문제를 풀 때 문제 상황을 2-SAT 문제로 모델링하는 것이다. 여기에서 몇 가지 응용의 예를 살펴보자.
사실 여러 종류의 연산들을 구현해놓은 라이브러리가 있다.
https://github.com/kth-competitive-programming/kactl/blob/main/content/graph/2sat.h
기본적인 응용
기본적인 논리식 조작을 통해 많은 문제를 2-SAT으로 만들 수 있다.
- $x \iff (x \lor x)$
- $x=y \iff (x \lor \bar y) \land (\bar x \lor y)$
- $\overline{x \land y} \iff (\bar x \lor \bar y)$
- $(x \land y) \lor (z \land w) \iff (x \lor z) \land (x \lor w) \land (y \lor z) \land (y \lor w)$
- $x \neq y \iff (x \lor y) \land (\bar x \lor \bar y)$ (하나가 참이고 하나가 거짓)
- $x = y \iff (x \lor \bar y) \land (\bar x \lor y)$
연습문제
- https://www.acmicpc.net/problem/11281
- 2-SAT을 구현하는 문제이다.
- https://www.acmicpc.net/problem/1154 (2-SAT 없이도 해결 가능)
- 학생 $i$가 $A$팀에 속하면 $x_i = true$ 로 보자. 만약, 학생 $i$와 학생 $ j$가 서로 안다면, 이들이 같은 팀에 속하든 다른 팀에 속하든 별 문제가 없다. 하지만, 두 학생이 서로 모른다면, 둘 중 한 명은 A팀, 다른 한 명은 B팀에 속한다. 이는 $(x_i \lor x_j) \land (\bar x_i \lor \bar x_j)$ 의 논리식으로 나타낼 수 있다.
- https://www.acmicpc.net/problem/16853
- https://www.acmicpc.net/problem/1739
- https://www.acmicpc.net/problem/20534
어떤 원소들 중 1개 이하가 참인 상황
예를 들어, $n$개의 변수 $x_1, x_2, \cdots, x_n$이 있고, $x_1, x_2, \cdots, x_n$ 중 최대 1개만이 참인 상황을 논리식으로 모델링하고 싶다고 하자.
$O(n^2)$ 기법
모든 $i \neq j$에 대해 $(\bar x_i \lor \bar x_j)$를 추가하면 된다.
$O(n)$ 기법
더미 변수 $n$개 $y_1, y_2, \cdots, y_n$을 추가할텐데, $y_i = x_1 \lor x_2 \lor \cdots \lor x_i$가 되게 할 것이다. 그러기 위해, 다음 세 가지 조건을 추가할 것이다.
- $x_i \to y_i$
- $y_i \to y_{i+1}$
- $y_i \to \bar x_{i+1}$
그러면, $O(n)$개의 더미 변수와 $O(n)$개의 식이 최종적으로 추가되게 된다. 이 방법을 이용하면 여러 문제를 해결할 수 있다.
연습문제
- https://www.acmicpc.net/problem/2519
- 막대 $i$를 지우는 것을 $x_i$라 하자. 그러면, $i$와 $j$가 교차하여 둘 중 하나가 사라져야 하는 경우에 대한 조건은 $(x_i \lor x_j)$ 가 되며, 3개의 막대 $i, j, k$ 중 최대 1개를 제거하는 것에 대한 조건은 위 섹션에서 설명한 방법으로 논리 식을 만들 수 있다.
- https://www.acmicpc.net/problem/19703
- $O(n)$ 기법을 구현하면 되는 문제다.
- https://www.acmicpc.net/problem/1733
- $O(n)$ 기법을 활용하지 않고도 풀 수 있으며, 활용해서도 풀 수 있다.
4. 2-SAT의 구현
아래는 2-SAT의 구현을 체크할 수 있는 BOJ의 11281번 2-SAT - 4 문제에 대한 필자의 코드다.
#include <stdio.h>
#include <algorithm>
#include <vector>
#include <utility>
using namespace std;
int N, M;
typedef vector<int> vi;
typedef vector<vi> vvi;
typedef pair<int, int> pii;
inline int bmod(int x, int y) { return (x+y)%y; }
// Kosaraju's SCC Algorithm
vvi reverse_edges(vvi &adj) {
vvi adj_rev;
adj_rev.resize(adj.size());
for (int i=0; i<adj.size(); i++) {
int u = i;
for (int j=0; j<adj[i].size();j++) {
int v = adj[i][j];
adj_rev[v].push_back(u);
}
}
return adj_rev;
}
void DFS(vvi &adj, int u, vi &visited, vi &node_stack) {
visited[u] = 1;
for (int i=0; i<adj[u].size();i++) {
int v = adj[u][i];
if (visited[v] == 0) DFS(adj, v, visited, node_stack);
}
node_stack.push_back(u);
}
vvi find_SCC(vvi &adj, vvi &adj_rev) {
vi vis_fw;
vi nd_st;
vis_fw.resize(adj.size(), 0);
for (int i=0; i<adj.size(); i++) {
if (vis_fw[i] == 0) DFS(adj, i, vis_fw, nd_st);
}
vi vis_bw;
vvi sccs;
vis_bw.resize(adj_rev.size(), 0);
for (int i=0; i<adj_rev.size(); i++) {
int u = nd_st.back();
nd_st.pop_back();
if (vis_bw[u]==0) {
vi scc;
DFS(adj_rev, u, vis_bw, scc);
sccs.push_back(scc);
}
}
return sccs;
}
// Reducing 2-SAT into SCC
void build_graph(vector<pii> &P, vvi &adj) {
int k = P.size();
int n = N;
adj.resize(2*n);
vi perm;
perm.push_back(0);
for (int i=1; i<n+1; i++) perm.push_back(n-1+i);
perm.push_back(0);
for (int i=n; i>0; i--) perm.push_back(n-i);
int m = perm.size();
for (int j=0; j<k; j++) {
int u = P[j].first, v = P[j].second;
adj[perm[bmod(-u, m)]].push_back(perm[bmod(v, m)]);
adj[perm[bmod(-v, m)]].push_back(perm[bmod(u, m)]);
}
}
// 2-SAT Solver
vi solve(vector<pii> &P) {
vvi adj, adj_rev;
int n = N;
build_graph(P, adj);
adj_rev = reverse_edges(adj);
vvi sccs = find_SCC(adj, adj_rev);
vi sccID;
sccID.resize(2*n+5);
int m = sccID.size();
for (int h=0; h<sccs.size(); h++) {
for (int i=0; i<sccs[h].size(); i++) {
int c = sccs[h][i];
if (n <= c) c -= n-1;
else c -= n;
sccID[bmod(c, m)] = h;
}
}
vi ans;
for (int i=1; i<n+1; i++) { if (sccID[i] == sccID[m-i]) return ans; }
for (int i=1; i<n+1; i++) ans.push_back((sccID[i] > sccID[m-i]));
return ans;
}
// Input/Output
int main(){
scanf("%d%d", &N, &M);
vector<pii> P;
for (int num = 0; num<M; num++) {
int i, j;
scanf("%d%d", &i, &j);
P.push_back(make_pair(i, j));
}
vi ans = solve(P);
if (ans.empty()) {
printf("0\n");
return 0;
}
printf("1\n");
for (int i=0; i<N; i++) printf("%d ", ans[i]);
return 0;
}