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

접근

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

11280번: 2-SAT - 3

$$f=(x_1\vee x_2)\wedge (x_2\vee x_3)\wedge (x_3\vee x_4)$$

위와 같은 식이 있을 때, f가 true 이기 위해서는 각각의 $x_1\vee x_2$ 요소들이 모두 true여야 한다. $x_1\vee x_2$ 가 true 이기 위해서는 $x_1$ 혹은 $x_2$가 true 여야 한다. 즉, $x_1$ 이 false 라면 $x_2$ 가 반드시 true 여야 하고, 반대로 $x_2$ 가 false 라면 $x_1$ 은 반드시 true 여야 한다. 이 선후 관계를 아래와 같이 표기할 수 있다.

$$\sim x_1\to x_2$$

$$\sim x_2\to x_2$$

주어진 식의 모든 요소들을 이와 같이 변환하여 그래프로 표현한다면, f 가 true 로 성립하기 위해서는 해당 그래프가 이루는 선후관계의 요소들이 모순되는 점이 없어야 할 것이다. 즉 SCC 로 해당 그래프를 분류하였을 때 같은 SCC에 $x_1$ 과 $\sim x_1$ 이 한꺼번에 포함되어 있다면 이는 모순이 발생하여 f 가 false 를 보이게 된다.

코드

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

using namespace std;

#define endl '\n'
#define MAX_N 22
#define MAX_M 101

int N, M;
vector<int> Path[MAX_N * 2];
int id, sccNum;
int scc_id[MAX_N * 2];
int scc_finished[MAX_N * 2];
int sn[MAX_N * 2];
stack<int> scc_stack;

int Not(int a) {
    return (N < a ? a - N : a + N);
}

// SCC 알고리즘
int dfs(int c) {
    scc_id[c] = ++id;
    scc_stack.push(c);
    int res = scc_id[c];
    for (int next : Path[c]) {
        if (scc_id[next] == 0) {
            res = min(res, dfs(next));
        } else if (!scc_finished[next]) {
            res = min(res, scc_id[next]);
        }
    }
    if (res == scc_id[c]) {
        // 같은 SCC 끼리는 같은 숫자의 sn[x] 값을 갖게 된다.
        while (1) {
            int t = scc_stack.top();
            scc_stack.pop();
            scc_finished[t] = 1;
            sn[t] = sccNum;
            if (t == c) break;
        }
        sccNum++;
    }
    return res;
}

// 같은 SCC 에 x 와 ~x 가 동시에 포함되는지 체크하는 함수
int Check() {
    for (int i = 1; i <= N; i++) {
        if (sn[i] == sn[i + N]) return 0;
    }
    return 1;
}

int main(int argc, char** argv) {
    // freopen 주석 처리
    freopen("input.txt", "r", stdin);

    ios::sync_with_stdio(false);
    cin.tie(NULL);
    cout.tie(NULL);

    cin >> N >> M;
    int a, b;
    for (int i = 0; i < M; i++) {
        cin >> a >> b;
        if (a < 0) a = -a + N;
        if (b < 0) b = -b + N;
        Path[Not(a)].push_back(b);
        Path[Not(b)].push_back(a);
    }
    for (int i = 1; i <= 2 * N; i++) {
        if (scc_id[i] == 0) dfs(i);
    }
    if (Check()) {
        cout << 1 << endl;
    } else {
        cout << 0 << endl;
    }

    return 0;
}

더 생각해 볼 것?

...

코드나 내용 관련 조언, 부족한 점 및 질문 언제든 환영합니다!