문제

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


알고리즘

2-SAT


풀이

SCC알고리즘을 활용하여 2-SAT을 모델링하는 문제입니다.

True나 False를 판단해야 하는 하나의 변수에 대해 이미 True나 False를 정해주고 모순이 생기는지만 확인하는 문제입니다. 각 절에 대해 두 개의 or 관계가 주어지면 우리가 얻을 수 있는 정보는 다음과 같습니다. A or B가 주어졌을 때 False A 라면 True B 여야 하고, False B 라면 True A 여야만 합니다.

두 개의 정보에 대해 우리는 간선으로 표현할 수 있으며, 만약 하나의 정점 C에 대해 False C와 True C가 동일한 컴포넌트로 묶인다면 이는 모순임을 나타냅니다.

변수는 1부터 시작하므로 크기를 할당할 때 $N+1$임을 생각하도록 합시다. 이 문제는 비교적 간단하기 때문에 굳이 OR 함수를 작성하지 않아도 되지만, 문제가 어려워질수록 헷갈려지기 때문에 디버깅의 편의를 위해 OR함수를 작성하시는 것을 추천드립니다. 시간 복잡도는 $O(V+E)$입니다.

코드

#include <bits/stdc++.h>
#define rep(i,n) for(int i=0;i<n;++i)
#define REP(i,n) for(int i=1;i<=n;++i)
#define FAST cin.tie(NULL);cout.tie(NULL); ios::sync_with_stdio(false)
using namespace std;

#define t(x) (x<<1)
#define f(x) (x<<1|1)
#define W(x) (x>0?t(x-1):f(-(x+1)))

int N, M, u, v, VC, SC;

vector<vector<int>> adj;
vector<int> discovered, sccid;
stack<int> st;
void OR(int u, int v) {
    adj[W(u) ^ 1].emplace_back(W(v));
    adj[W(v) ^ 1].emplace_back(W(u));
}

int scc(int here) {
    int ret = discovered[here] = VC++;
    st.emplace(here);
    for (auto there : adj[here]) {
        if (discovered[there] == -1) ret = min(ret, scc(there));
        else if (sccid[there] == -1) ret = min(ret, discovered[there]);
    }

    if (ret == discovered[here]) {
        while (1) {
            int t = st.top();
            st.pop();
            sccid[t] = SC;
            if (t == here) break;
        }
        ++SC;
    }
    return ret;
}

int main() {
    FAST;

    cin >> N >> M;
    adj.resize(N << 1);
    rep(i, M) {
        cin >> u >> v;
        OR(u, v);
    }
    discovered = sccid = vector<int>(N << 1, -1);
    rep(i, N << 1) if (discovered[i] == -1) scc(i);
    bool flag = 1;
    rep(i, N) if (sccid[t(i)] == sccid[f(i)]) {
        flag = 0;
        break;
    }
    cout << flag;

    return 0;
}