2-SAT(satisfiability)

2-SAT(satisfiability) 문제는 n개의 bool 변수로 이루어진 2-CNF 식이 true가 되게 하는 경우가 있는지, 있다면 각 변수에는 어떤 값이 들어가야 하는지 정하는 문제이다. 이 문제에서 2-SAT이 무엇인지 잘 설명해주고 있다.
참고로 3-SAT(또는 SAT)는 NP-complete 문제이다.(Cook-Levin theorem)

그래프 모델링

$f = (\neg x1 \lor x2) \land (\neg x2 \lor x3) \land (x1 \lor x3) \land (x3 \lor x2) $인 경우를 보자.
이때 ￢는 not, ∨은 or, ∧는 and 이다.

먼저 $(\neg x1 \lor x2)$이 참이 되기 위해서는 $\neg x1$이 참이거나, $x2$가 참이면 된다.

1. $\neg x1$이 참이라면, $x2$는 어떤 값이든 무관하다.(don’t care)
2. $x2$가 참이라면, $\neg x1$는 어떤 값이든 무관하다.(don’t care)

하지만 $\neg x1$이 거짓이라면, $x2$는 반드시 참이어야 한다. 마찬가지로 $x2$가 거짓이라면, $\neg x1$은 반드시 참이어야 한다. 따라서 2개의 명제를 만들 수 있다. 또한 두 명제는 대우 관계이다.

1. $\neg x1$이 거짓이라면, $x2$는 반드시 참이어야 한다.: $x1 \rightarrow x2$
2. $x2$가 거짓이라면, $\neg x1$은 반드시 참이어야 한다.: $\neg x2 \rightarrow \neg x1$

따라서 CNF을 이루는 각 절(clause)은 2개의 명제로 바꿀 수 있고, 우리는 각 명제를 만족하는지 확인하면 된다.
이를 구현하기 위해 그래프로 모델링한다. 각 정점들은 xi와 ￢xi에 대응시키고, 명제의 가정과 결론을 엣지로 연결시킨다.

예를 들어, $(x1, x2, \neg x1, \neg x2)$를 정점 (1, 2, 3, 4)에 각각 대응시킨다면, 명제 $(\neg x1 \lor x2)$는 그래프상에서 (1→2), (4→3)으로 나타내면 된다.

2-SAT 판정 방법

명제들 중에서 하나라도(any) 명제를 만족하지 않는 경우는 어떻게 검출할까. 우리는 위에서 각 절이 2개의 명제를 만든다는 것을 알았다. 이 명제들을 모두 만족한다면 주어진 2-CNF는 true가 될 수 있는 경우가 존재한다는 것이다.

모든 명제들이 성립되려면, 각 명제들이 서로 모순되면 안된다. $x1 \rightarrow \neg x1$, $\neg x1 \rightarrow x1$ 꼴의 명제가 동시에 존재해서는 안된다.
명제 $x1 \rightarrow \neg x1$가 참이 되려면 $x1$이 false 이어야한다. 논리학에서는 이것을 vacuous truth 라고 부른다. 전제가 거짓이면 명제는 항상 참이다. 같은 이유로 $\neg x1 \rightarrow x1$가 참이 되려면 $x1$이 true이면 된다. 따라서 $x1 \rightarrow \neg x1$, $\neg x1 \rightarrow x1$ 명제가 동시에 존재하면 안된다.

2개의 명제 $a \rightarrow b, b \rightarrow c$가 있다고 하자. 우리는 이 명제들을 이용해 새로운 명제($a \rightarrow c$)를 추론할 수 있다. 명제들끼리 삼단 논법과 같은 추론을 계속 적용시켰을 때, 모순이 발생하지 않아야 한다. 명제를 그래프로 모델링한다면, 명제 추론은 ‘정점 a에서 정점 b로 가는 경로(path)가 있다.’로 바꿀 수 있다.

결론적으로 정점 xi에서 ￢xi로 가는 경로가 양쪽으로 존재하면 안된다. 이는 두 정점이 같은 SCC에 있으면 안되는 경우로 바꿀 수 있다. 따라서 2-SAT 문제는 SCC 문제이기도 하다.

---

문제 예시 및 코드

백준 11280

#include <iostream>
#include <algorithm>
#include <vector>
#include <stack>
using namespace std;

int n, m;
vector<int> edge[20002];
int d[20002], id = 0, sccNum; // scc 개수
int sn[20002]; // i가 속한 SCC의 번호
bool finished[20002]; // SCC 성립되면 true
stack<int> s;

inline int oppo(int a) {
    return a <= n ? a + n : a - n;
}

void input() {
    cin >> n >> m;
    int a, b;
    for (int i = 0; i < m; ++i) {
        cin >> a >> b;
        if (a < 0) a = -a + n;
        if (b < 0) b = -b + n;
        edge[oppo(a)].push_back(b);
        edge[oppo(b)].push_back(a);
    }
}

int DFS(int here) {
    d[here] = ++id; // 정점에 고유 id 할당
    s.push(here); // 스택에 자신을 삽입

    int result = d[here];
    for (int next: edge[here]) {
        if (d[next] == 0) result = min(result, DFS(next));
        else if (!finished[next]) result = min(result, d[next]);
    }

    if (result == d[here]) {
        while (1) {
            int t = s.top();
            s.pop();
            finished[t] = true;
            sn[t] = sccNum;
            if (t == here) break;
        }
        sccNum++;
    }
    return result;
}

int main() {
    input();

    // SCC 구하기
    for (int i = 1; i <= n; i++) {
        if (d[i] == 0) DFS(i);
        if (d[i + n] == 0) DFS(i);
    }

    for (int i = 1; i <= n; ++i) {
        if (sn[i] == sn[i + n]) {
            // a와 not a가 같은 SCC에 속한다면 f는 true가 절대 불가능
            cout << 0;
            return 0;
        }
    }
    cout << 1;
}