2-SAT(satisfiability)

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

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

먼저 (￢x1∨ x2)이 참이 되기 위해서는 ￢x1이 참이거나, x2가 참이면 된다.

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

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

1. ￢x1이 거짓이라면, x2는 반드시 참: x1 → x2
2. x2가 거짓이라면, ￢x1은 반드시 참: ￢x2 → ￢x1

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

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

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

모든 명제들이 성립되려면, 각 명제들이 서로 모순되면 안된다. 예를 들어, x1→x1, ￢x1→x1 꼴의 명제가 동시에 존재해서는 안된다.
2개의 명제 a→b, b→c가 있다고 하자. 우리는 이 명제들을 이용해 새로운 명제(a→c)를 추론할 수 있다. 명제들끼리 삼단 논법과 같은 추론을 계속 적용시켰을 때, 모순만 발생하지 않으면 된다.

명제를 그래프로 모델링한다면, 명제 추론은 '정점 a에서 정점 b로 가는 길(path)가 있다.'로 바꿀 수 있다. 따라서 정점 xi에서 ￢xi로 가는 경로가 양쪽으로 존재하면 안된다. 이는 두 정점이 같은 SCC에 있으면 안되는 경우로 바꿀 수 있다. 따라서 2-SAT 문제는 SCC 문제이기도 하다.

---

2-SAT - 3

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