[C++] 2-SAT - 3 (백준 11280번) - 2-SAT

https://www.acmicpc.net/problem/11280

 

2개의 변수가 or 연산으로 결합된 절 여러 개가 and 연산으로 결합된 식을 2-CNF 식이라고 한다.

이러한 2-CNF 식이 true가 되도록 하는 문제를 2-SAT 문제라고 하고, 2-SAT 문제는 SCC를 통해서 해결할 수 있음이 알려져 있다.

 

그 이유는 다음과 같다.

 

전체 식이 true가 되려면 각 절은 모두 true가 되어야 한다.

a or b 라는 절이 true가 되려면, a가 false면 b가 반드시 true여야 하고 b가 false면 a가 반드시 true여야 한다.

 

이제 어떤 정점이 참일 때 다른 어떤 정점도 연쇄적으로 참이 되어야 한다는 것을 그래프로 표현해보자.

a or b 라는 절에 대해서는 그래프에 ~a -> b 간선과 ~b -> a 간선을 만들어주면 된다.

이 그래프에서 SCC를 구할 수 있는데, 이 때 같은 컴포넌트 안에 있는 정점들을 전부 서로 영향을 주는 관계이기 때문에 하나가 참이면 전체가 참이어야 한다.

 

x와 ~x가 같은 컴포넌트 안에 있다는 것은 모순이 발생한다는 뜻이다.

왜냐하면 하나의 컴포넌트에 속해 있는 정점들 중 하나라도 참이면 나머지가 모두 참이 되어야 하기 때문이다.

따라서 마지막에 x와 ~x가 같은 컴포넌트 안에 있는 경우가 없는지만 확인해주면 된다.

 

나는 코사라주 알고리즘을 통해 SCC를 구하고 각 정점이 속하는 컴포넌트의 번호를 scc 배열에 저장해두었다.

그리고 마지막에 scc[x] == scc[~x] 인 경우가 존재하는지 체크해주었다.

 

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

int n, m, idx;
vector<vector<int>> adj1;
vector<vector<int>> adj2;
vector<bool> vst;
stack<int> stk;
vector<int> scc;

void dfs1(int cur) {
    vst[cur] = true;
    for (int nxt: adj1[cur]) {
        if (!vst[nxt]) dfs1(nxt);
    }
    stk.push(cur);
}

void dfs2(int cur) {
    vst[cur] = true;
    scc[cur] = idx;
    for (int nxt: adj2[cur]) {
        if (!vst[nxt]) dfs2(nxt);
    }
}

int neg(int x) {
    if (x <= n) return x + n;
    else return x - n;
}

void solve() {
    cin >> n >> m;

    adj1 = vector<vector<int>>(2 * n + 1);
    adj2 = vector<vector<int>>(2 * n + 1);

    for (int i = 0; i < m; i++) {
        int a, b;
        cin >> a >> b;

        if (a < 0) a = -a + n;
        if (b < 0) b = -b + n;

        adj1[neg(a)].push_back(b);
        adj1[neg(b)].push_back(a);
        adj2[b].push_back(neg(a));
        adj2[a].push_back(neg(b));
    }

    vst = vector<bool>(2 * n + 1, false);
    for (int i = 1; i < 2 * n + 1; i++) {
        if (!vst[i]) dfs1(i);
    }

    idx = 0;
    scc = vector<int>(2 * n + 1, -1);
    vst = vector<bool>(2 * n + 1, false);
    while (!stk.empty()) {
        int x = stk.top();
        stk.pop();
        if (!vst[x]) {
            dfs2(x);
            idx++;
        }
    }

    for (int i = 1; i < n + 1; i++) {
        if (scc[i] == scc[neg(i)]) {
            cout << 0 << '\n';
            return;
        }
    }

    cout << 1 << '\n';
}

int main() {
    ios_base::sync_with_stdio(0);
    cin.tie(0);

    int T = 1;
    for (int i = 0; i < T; i++) {
        solve();
    }
}

(AC)