[C++] 2-SAT - 4 (백준 11281번) - 2-SAT with 역추적

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

 

2-SAT - 3 문제에 역추적만 추가된 문제이다. 2-SAT - 3 문제의 풀이는 이 글에서 확인할 수 있다.

 

이전 글에서 a or b 라는 절에 대해 ~a -> b 간선과 ~b -> a 간선을 만들어서 그래프를 구성하고, 그 그래프에서 SCC를 구해서 x와 ~x가 같은 컴포넌트에 속해 있는 경우가 없어야 한다는 것까지 알았다.

이제 가능한 경우에 대해서, 각 변수를 어떻게 둬야 전체 식이 true가 되는 건지를 알고 싶은 것이다.

 

그래프를 구성하고 SCC를 구하는 것까지는 동일하다. SCC를 구한 다음에 scc 배열을 보면서 어떤 변수를 true로 설정해야 하는지만 결정해주면 된다.

 

우선 x 정점과 ~x 정점이 있을 때, 그 두 정점이 가질 수 있는 관계는 세 가지이다.

1. x 정점이 속한 컴포넌트와 ~x 정점이 속한 컴포넌트가 같다.

2. x 정점이 속한 컴포넌트에서 ~x 정점이 속한 컴포넌트로의 간선이 있다. (또는 그 반대 방향의 간선이 있다.)

3. x 정점이 속한 컴포넌트와 ~x 정점이 속한 컴포넌트는 서로 연결되어 있지 않다.

 

1번의 경우는 모순이 생기는 경우, 즉 전체 식을 true로 만드는 것이 불가능한 경우이다.

 

2번의 경우에서는 뒤쪽 정점이 true가 되도록 설정해야 한다.

왜냐하면 우리가 설계한 그래프 상 앞쪽 정점이 true가 되면 뒤쪽에 연결된 정점들이 모두 true가 되어야 하기 때문에, 앞쪽 정점과 뒤쪽 정점 중 하나면 true가 되도록 하고 싶은 경우라면 반드시 뒤쪽 정점을 true로 두고 앞쪽 정점은 false로 둬야 한다.

 

3번의 경우는 서로 영향을 주지 않는 경우이므로 어떻게 설정하든 상관이 없다.

 

따라서, 모든 x와 ~x에 대해서 scc 배열 값을 비교하면서 더 뒤쪽인 정점, 즉 scc 배열 값이 더 큰 정점이 true가 되도록 출력해주면 된다.

 

#include <iostream>
#include <vector>
#include <stack>
#include <algorithm>
using namespace std;

int n, m, idx;
vector<vector<int>> adj1;
vector<vector<int>> adj2;
vector<int> vst;
stack<int> stk;
vector<int> scc;

void dfs1(int cur) {
    vst[cur] = true;
    for (int nxt: adj1[cur]) {
        if (!vst[nxt]) dfs1(nxt);
    }
    stk.push(cur);
}

void dfs2(int cur) {
    vst[cur] = true;
    scc[cur] = idx;
    for (int nxt: adj2[cur]) {
        if (!vst[nxt]) dfs2(nxt);
    }
}

int neg(int x) {
    if (x <= n) return x + n;
    else return x - n;
}

void solve() {
    cin >> n >> m;

    adj1 = vector<vector<int>>(2 * n + 1);
    adj2 = vector<vector<int>>(2 * n + 1);

    for (int i = 0; i < m; i++) {
        int a, b;
        cin >> a >> b;

        if (a < 0) a = -a + n;
        if (b < 0) b = -b + n;

        adj1[neg(a)].push_back(b);
        adj1[neg(b)].push_back(a);
        adj2[b].push_back(neg(a));
        adj2[a].push_back(neg(b));
    }

    vst = vector<int>(2 * n + 1, false);
    for (int i = 1; i < 2 * n + 1; i++) {
        if (!vst[i]) dfs1(i);
    }

    idx = 0;
    scc = vector<int>(2 * n + 1, -1);
    vst = vector<int>(2 * n + 1, false);
    while (!stk.empty()) {
        int x = stk.top();
        stk.pop();
        if (!vst[x]) {
            dfs2(x);
            idx++;
        }
    }

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

    cout << 1 << '\n';
    
    for (int i = 1; i < n + 1; i++) {
        if (scc[i] > scc[neg(i)]) cout << 1 << ' ';
        else cout << 0 << ' ';
    }
    cout << '\n';
}

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

    int T = 1;
    for (int i = 0; i < T; i++) {
        solve();
    }
}

(AC)

 

[참고] https://qwaz.io/posts/scc-and-2-sat