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$의 관계를 생각해보면 다음 세 가지 중 하나이다.

1. $x_i \to \bar x_i$ 경로와 $\bar x_i \to x_i$ 경로가 모두 존재한다.
2. $x_i \to \bar x_i$ 경로와 $\bar x_i \to x_i$ 경로 중 하나만 존재한다.
3. $x_i, \bar x_i$ 사이에 어느 방향의 경로도 존재하지 않는다.

위 세 경우에 대해 생각해보면,

1. 이 경우에는 $x_i \to \bar x_i$ 이고, $x_i \leftarrow \bar x_i$ 라 $x_i \Leftrightarrow \bar x_i$ 가 되고, 이는 모순이다. 고로, 이러한 경우가 존재하면, 충족 가능하지 않다.
2. 이 두 경로 중 하나만 존재한다면, "가정이 거짓인 명제는 항상 참"이기 때문에, "결론 부분에 오는 정점", 즉, 위상정렬 순서가 더 늦은 쪽이 참이 된다.
3. 이 경우는 딱히 고려할게 없어서 해피한 경우다.

따라서, 다음의 과정을 통해 2-SAT 문제를 풀 수 있다:

1. 2-CNF 식으로 부터 그래프를 구성한다. (참고로, 이 그래프는 implication graph라 부른다.)
2. SCC로 그래프를 분해한다.
3. $x_i, \bar x_i$ 가 같은 SCC에 속하는 경우가 있으면, unsatisfiable이라 결론 내린다.
4. 그렇지 않다면, 각 $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;
}

void build_graph(vector<pii> &P, vvi &adj) {
    int k = P.size();
    int n = N;
    adj.resize(2*n+1);
    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)]);
    }
} 

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+1);
    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;
}

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;
}