백준 [11280] 2-SAT - 3

문제 설명

문제 링크

http://icpc.me/11280

11280번: 2-SAT - 3

풀이

이 문제는 SCC를 구하기 위해 코사라주 알고리즘을 이용한다.

 (xi V xj)가  항상 참이기 위해서는 xi 가 거짓이라면 xj는 항상 참이어야 한다. 또한 반대로 xj 가 거짓이라면 xi는 항상 참이어야 한다.

그렇기 때문에 not(xi) -> xj와 not(xj) -> xi 간선을 만든다. 이것은 위의 설명을 그래프로 나타낸 것이다.

이때 한 SCC안에 xi와 not(xi)가 존재한다면 xi 가 참일 때 not(xi)와 xi 모두 참이어야 하는 것을 의미하고 이것은 모순이다.

그렇기 때문에 이때 0을 출력한다.

코드

#include <cstdio>
#include <vector>
#include <stack>
#include <cstring>

using namespace std;

vector<int> v[20004], rev[20004];
bool visited[20004];
stack<int> s;
int scc[20004];

inline int notX(int x) { return x ^ 1; } // not은 1부분만 반전된 것이므로 1부분만 xor한다
inline int trueX(int x) { return x << 1; } // 참인 것은 2배를 한다
inline int falseX(int x) { return x << 1 | 1; } // 거짓인 것은 2배를 하고 1을 더한다

void dfs(int cur) {
    visited[cur] = 1;
    for (auto nxt : v[cur]) {
        if (!visited[nxt]) dfs(nxt);
    }    
    s.push(cur);
}

void rev_dfs(int cur, int idx) {
    visited[cur] = 1;
    scc[cur] = idx;
    for (auto nxt : rev[cur]) {
        if (!visited[nxt]) rev_dfs(nxt, idx);
    }
}

void getSCC(int n) {
    memset(visited, 0, sizeof visited);
    for (int i = 2; i <= 2 * n + 1; i++) {
        if (!visited[i]) dfs(i);
    }

    memset(visited, 0, sizeof visited);
    int idx = 1;
    while (!s.empty()) {
        int cur = s.top(); s.pop();
        if (!visited[cur]) {
            rev_dfs(cur, idx);
            idx++;
        }
    }
}

int main() {
    int n, m; scanf("%d %d", &n, &m);
    while (m--) {
        int a, b; scanf("%d %d", &a, &b);
        a = (a > 0 ? trueX(a) : falseX(-a));
        b = (b > 0 ? trueX(b) : falseX(-b));

        v[notX(a)].push_back(b);
        rev[b].push_back(notX(a));
        v[notX(b)].push_back(a);
        rev[a].push_back(notX(b));
    }

    getSCC(n);

    for (int i = 1; i <= n; i++) {
        if (scc[trueX(i)] == scc[falseX(i)]) {
            printf("0");
            return 0;
        }
    }
    printf("1");
}

참고

https://justicehui.github.io/hard-algorithm/2019/05/17/2SAT/

[그래프] 2-SAT문제 - 1

https://blog.qwaz.io/problem-solving/scc%EC%99%80-2-sat

SCC와 2-SAT