백준 2-SAT - 4 C++

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

2-SAT 문제를 공부해보았습니다.

 

2-SAT문제는 아래와 같습니다.

(x or y) : clause 를 대상으로 CNF 형태 (모두 and로 묶여 있는 형태) 에 대해 해가 존재하는 지를 판단 (만족하는 해가 있는가?) 하는 satisfiability 문제입니다. 

 

x or y == ~x -> y

x or y == y or x == ~y -> x 이므로 CNF로 주어진 식을 아래와 같이 그래프로 표현할 수 있습니다. 

 

ex) (~x1 or x2) and (~x2 or x3) and (x1 or x3) and (x3 or x2) 

x1 -> x2, ~x2 -> ~x1

x2 -> x3, ~x3 -> ~x2

~x1 -> x3, ~x3 -> x1

~x3 -> x2, ~x2 -> x3

 

이제 이 그래프를 대상으로 SCC를 구합니다. SCC를 구하면, cycle 관계의 컴포넌트를 구상할 수 있으며, 코사라주 알고리즘을 기준으로는 생성된 SCC 순으로 위상정렬됩니다. (타잔은 역순)

 

즉 위 그래프에 대해서 코사라주 알고리즘으로 SCC를 계산하면 다음과 같습니다. 

x1, ~x1, x2, ~x2, x3, ~x3 순으로 탐색

=> x1 -> x2 -> x3 => stack : x3, x2, x1

=> ~x1 (연결된 거 이미 다 방문) => stack : x3, x2, x1, ~x1

=> ~x2 (연결된 거 이미 다 방문) => stack : x3, x2, x1, ~x1, ~x2

=> ~x3 (연결된 거 이미 다 방문) => stack : x3, x2, x1, ~x1, ~x2, ~x3

 

stack에 저장된 순으로 역방향 그래프로 탐색

~x3 : 역방향에서 갈 곳 없음 => SCC1(~x3)

~x2 : 역방향에서 갈 곳 없음 => SCC2(~x2)

~x1 : 역방향에서 갈 곳 없음 => SCC3(~x1)

x1, x2, x3 : 마찬가지로 각각 역방향에서 더 이상 갈 곳 없음 => SCC4(x1), SCC5(x2), SCC6(x3) 

 

위상정렬 순서 : SCC1 -> SCC2 -> SCC3 -> SCC4 -> SCC5 -> SCC6

 

위 순서에 맞춰서 x -> ~x 인 경우, x = false, ~x -> x 인 경우, x = true 일 때 implication (->) 이 true를 만족하므로 적절한 x를 구하면 됩니다.

즉, 코사라주 알고리즘 기준으로, x의 scc 번호를 scc[x]라 하면

scc[x] < scc[~x] : x = false, scc[~x] < scc[x] : x = true 입니다. 

 

주어진 명제가 해가 없는 경우는, scc[x] == scc[~x] 인 경우입니다. 

이는 동일 scc에 있는 것은 cycle이 있는 것이므로, x->~x, ~x->x 를 의미하므로, 이는 모순인 케이스이기 때문입니다. 

 

코드는 아래와 같습니다. 

#include <vector>
#include <algorithm>
#include <stack>
#include <iostream>

using namespace std;

int N, M;
// 음수에 대한 인덱스 계산을 위해 아래와 같이 인덱스 부여 
// a > 0: a<<1, a < 0 : a<<1 | 1

// a or b == (~a -> b) / (~b -> a)

vector<int> graph[10001 << 1];
vector<int> invGraph[10001 << 1];
bool visited[10001 << 1];
bool invVisited[10001 << 1];
vector<vector<int>> scc;
int sccIdx[10001 << 1];
stack<int> stk;

void init() {
    cin >> N >> M;
    int A, B;
    int a, b, na, nb;
    for(int i = 0; i < M; i++) {
        cin >> A >> B;
        if(A > 0) {
            a = A << 1;
            na = A << 1 | 1;
        } else {
            a = -A << 1 | 1;
            na = -A << 1;
        }

        if(B > 0) {
            b = B << 1;
            nb = B << 1 | 1;
        } else {
            b = -B << 1 | 1;
            nb = -B << 1;
        }

        graph[na].push_back(b);
        invGraph[b].push_back(na);
        graph[nb].push_back(a);
        invGraph[a].push_back(nb);
    }
}

void dfs(int node) {
    if(visited[node]) return;

    visited[node] = true;
    for(auto v : graph[node]) {
        if(visited[v]) continue;
        dfs(v);
    }

    stk.push(node);
    return;
}

void invDfs(int node, vector<int> &vec) {
    if(invVisited[node]) return;

    invVisited[node] = true;
    vec.push_back(node);

    for(auto v : invGraph[node]) {
        if(invVisited[v]) continue;
        invDfs(v, vec);
    }

    return;
}

void getSCC() {
    for(int node = 1; node <= (N << 1 | 1); node++) {
        dfs(node);
    }

    int idx = 0;
    while(!stk.empty()) {
        int node = stk.top();
        stk.pop();

        vector<int> vec;
        invDfs(node, vec);

        if(!vec.empty()) {
            scc.push_back(vec);
            for(auto v : vec) {
                sccIdx[v] = idx;
            }
            idx++;
        }
    }
}

bool calc() {
    // x, ~x 같이 있으면 false, 아니면 true
    for(int i = 1; i <= N; i++) {
        if(sccIdx[i << 1] == sccIdx[i << 1 | 1])
            return false;
    }
    return true;
}

void getAnswer() {
    vector<bool> answer(N+1, false);

    for(int node = 1; node <= N; node++) {
        if(sccIdx[node << 1] < sccIdx[node << 1 | 1]) {
            // x -> ~x : x = false
            answer[node] = false;
        } else {
            // ~x -> x : x = true 
            answer[node] = true;
        }
    }

    for(int i = 1; i <= N; i++) {
        cout << answer[i] << ' ';
    }
}

int main() {
    ios_base :: sync_with_stdio(false);
    cin.tie(NULL);
    cout.tie(NULL);

    init();
    getSCC();
    if(calc() == false) {
        cout << 0;
    } else {
        cout << 1 << '\n';
        getAnswer();
    }
    return 0;
}