[백준 11280] 2-SAT - 3

 

 그래프 이론을 이용해 푸는 2-SAT 문제. 처음 풀어보는 유형의 문제라, 알고 있는 알고리즘들을 다양하게 떠올려 풀어보려 했지만 마땅한 로직을 찾아내기 힘들었다. 논리식을 유심히 관찰했는데, 여러 가지 관계를 떠올릴 순 있었으나 제 시간 내에 해결할 수 있는 알고리즘으로 잘 연결되지 않았다.

 

 그래서 한참 고민 하다가, 관련된 내용을 찾아봤더니 SCC(Strongly Connected Component)를 이용해서 해결하는 어느정도 정형화된 로직이 있는 것 같았다. 읽으면서 처음 이렇게 접근할 생각을 한 사람이 누구일까 싶었다. 그리고 SCC를 빠르게 찾아내는 알고리즘들도 함께 찾아봤는데, 이건 그래프 문제들을 풀 때 정말 도움이 많이 될 것 같았다.

 

 일단 논리식으로부터 접근하는데, 문제의 각 절들이 모두 true가 되어야 한다는 사실은 누구나 관찰할 수 있을 것이다. 그리고 각 절이 true가 되기 위해서는 당연하게도 두 변수 중 한 변수는 true가 되어야 한다. 이는 둘 중 한 변수가 false인 경우, 나머지 한 변수는 true로 확정해야 한다는 소리이고 이를 그래프로 나타내볼 수 있다.

 만약에 절 하나가 (x V y)라면 ~x -> y 와 ~y -> x로 생각할 수 있다. 이렇게 논리식에서 변수들의 요구 조건을 그래프로 나타낸 것이 함축 그래프라고 한다. 모든 절에 대해서, 함축 그래프를 완성해 주고 SCC를 구해준다. 

 이 때, 어떤 변수 x와 그 역인 ~x가 같은 SCC에 속해있다면, x->~x인 경로와 ~x->x인 경로가 모두 연결 요소 내에 존재한다는 소리가 된다. 이는 x와 ~x가 모두 true가 되어야 함을 의미하며, 이는 모순으로 불가능하다. 따라서 SCC를 모두 구한 뒤에 변수와 그 변수의 역이 한 SCC에 속한 경우가 있다면, 식 f는 false가 되며 그 외의 경우엔 true가 된다.

 

 SCC를 구하는 알고리즘은 코사라주 알고리즘을 사용했다. 일단 그쪽이 구현이 간편해서 사용했는데, 다음에 SCC를 구하는 문제가 또 나오면 타잔 알고리즘도 사용해 봐야겠다.

#include <iostream>
#include <vector>
#include <unordered_set>
#include <stack>

using namespace std;

int n, m;
vector<unordered_set<int> > cnfGraph;
vector<unordered_set<int> > revCnfGraph; 
stack<int> st;
vector<bool> isVisited;
vector<int> scc;
int sccInd = 0;

void dfs(int x) {
    if(isVisited[x]) return;
    isVisited[x] = true;
    for(int adj: cnfGraph[x]) {
        if(!isVisited[adj]) {
            dfs(adj);
        }
    }
    st.push(x);
}

void reDfs(int x) {
    if(isVisited[x]) return;
    isVisited[x] = true;
    scc[x] = sccInd;
    for(int adj: revCnfGraph[x]) {
        if(!isVisited[adj]) {
            reDfs(adj);
        }
    }
}

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

    cin >> n >> m;
    cnfGraph = vector<unordered_set<int> >(2*n+1);
    revCnfGraph = vector<unordered_set<int> >(2*n+1);
    isVisited = vector<bool>(n*2+1, false);
    scc = vector<int>(n*2+1);

    for(int i=0; i<m; i++) {
        int u, v;
        cin >> u >> v;

        cnfGraph[n-u].insert(v+n);
        cnfGraph[n-v].insert(u+n);
        revCnfGraph[v+n].insert(n-u);
        revCnfGraph[u+n].insert(n-v);
    }

    for(int i=0; i<n; i++) {
        dfs(i);
    }
    for(int i=n+1; i<=n*2; i++) {
        dfs(i);
    }

    isVisited = vector<bool>(n*2+1, false);

    while(!st.empty()) {
        auto cur = st.top();
        st.pop(); 
        if(!isVisited[cur]) {
            sccInd++;
            reDfs(cur);
        }
    }

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

    cout << "1";
}