[백준] 11281: 2-SAT - 4

0. 문제 주소

 

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

11281번: 2-SAT - 4

 

 

1. 풀이

 

2-CNF(Conjunctive Normal Form)의 정의 : OR 연산만으로 연결된 괄호 단위(절, closure)들의 AND 연산만으로 이루어진 논리식.

 

2-SAT 문제는 각 closure의 변수가 최대 2개인 경우를 의미.

 

boolean expression의 각 변수에 true / false를 대입해서 전체 식이 true가 될 수 있는지, 가능하다면 어떻게 넣어야 하는지 찾는 문제를 satisfiability problem이라고 한다.

 

 

SCC를 이용해서 구한다.

 

먼저 변수가 N개라면, 1개의 변수 x에 대해 x, ~x가 가능하므로 총 2N개의 노드가 생긴다.

 

모든 절에 대해서 각 절마다 아래와 같은 방법으로 간선 두 가지를 추출한다.

 

ex) (x_i or x_j) 에 대해, !x_i => x_j  // !x_j => x_i

 

모든 절들이 and 연산으로 이루어져 있으므로 전체 식이 true가 되려면 모든 절이 true가 되어야 한다.

 

따라서 절 안의 or 연산으로 연결되어있는 변수에 대해, 만약 둘 중의 하나가 false라면 다른 하나는 반드시 true여야 한다는 아이디어에서 출발하고, 이를 그래프 간선으로 표시한다.

 

모든 절에 대해 간선을 추출하여 그래프를 만들고, SCC를 구성한다.

 

만약 동일한 SCC 내에, x_i와 !x_i가 함께 있다면 모순이 생긴다. SCC의 정의를 생각해 볼 때 당연하다.

 

따라서 위와 같이 한 SCC 안에 원래 변수, NOT 처리된 변수가 함께 있다면 전체 식을 true로 만들 수 없다는 결론을 내릴 수 있다.

 

 

만약 가능하다면, 어떤 변수를 넣어야 하는지도 찾을 수 있다.

 

p => q에서 만약 p가 거짓이라면 q의 결과는 이 명제에 영향을 미치지 않는다는 아이디어에서 출발한다.

 

SCC 단위로 위상정렬한 순서에 따라 그래프를 방문하며 아직 정해지지 않은 변수에 대해 false라고 설정해주면 된다.

 

이것이 가능한 이유를 생각해보기 위해선 어떤 상황에서 전체의 식을 true로 만드는 것에 실패하는지부터 생각하면 된다.

 

true => false로 가는 경로가 발생한다면 명제가 false가 되므로 이러한 경우를 만들면 안 된다.

 

p 노드와 !p 노드에 대해, WLOG p 노드를 먼저 방문했다고 하자. p를 false로 설정해주면, !p는 자동으로 true로 설정된다.

 

이미 satisfiability를 체크했기 때문에 p와 !p는 반드시 다른 노드에 존재할 수밖에 없고, p가 먼저 방문되었으므로 p가 속한 SCC에서 !p가 속한 SCC로 가는 경로는 존재할 수 있다.

 

하지만 SCC 단위의 그래프는 반드시 DAG이고, 만약 그러한 경로가 존재했다면 !p가 속한 SCC에서 p가 속한 SCC로 가는 길은 절대 존재할 수 없다.

 

따라서 false -> true 경로는 존재할 수 있어도, true -> false 경로는 생기지 않는다. 

 

 

번외로, dfs ordering의 순서를 뒤집으면 위상정렬의 순서가 된다. 코사라주 알고리즘이 이를 활용한다.

 

 

2. 풀이 코드

 

* 유의할 점

 

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

#define pii pair<int, int>
const int MAX = 10005;

using namespace std;

int N, M, sccnum, cnt;
int order[MAX*2], sn[MAX*2], ans[MAX];
bool finished[MAX*2];
vector<int> graph[MAX*2];
stack<int> st;
vector<pii> tsorder;

int makenot(int n){
    if (n%2) return n+1;
    else return n-1;
}

int dfs(int curr){
    order[curr] = ++cnt;
    st.push(curr);
    
    int ret = order[curr];
    for (int next: graph[curr]){
        if (order[next] == 0) ret = min(ret, dfs(next));
        else if (!finished[next]) ret = min(ret, order[next]);
    }
    if (ret == order[curr]){
        while(1){
            int t = st.top();
            st.pop();
            sn[t] = sccnum;
            finished[t] = true;
            if (t == curr) break;
        }
        sccnum++;
    }
    return ret;
}

int main() {
    #ifndef ONLINE_JUDGE
    freopen("input.txt", "r", stdin);
    #endif

    scanf("%d %d", &N, &M);
    int u, v;
    for (int i=0;i<M;i++){
        scanf("%d %d", &u, &v);
        u = u>0 ? u*2-1 : (-u)*2;
        v = v>0 ? v*2-1 : (-v)*2;
        graph[makenot(u)].push_back(v);
        graph[makenot(v)].push_back(u);
    }
    
    for (int i=1;i<=N*2;i++){
        if (order[i] == 0) dfs(i);
    }
    
    for (int i=1;i<=N;i++){
        if (sn[i*2-1] == sn[i*2]) {
            printf("0\n");
            return 0;
        }
    }
    printf("1\n");
    memset(ans, -1, sizeof(ans));
    for (int i=1;i<=N*2;i++){
        tsorder.push_back(pii(sn[i], i));
    }
    sort(tsorder.begin(), tsorder.end(), greater<pii>());
    for (auto p: tsorder){
        int curr = p.second;
        if (ans[(curr+1)/2] == -1){ // 1 : x1, 2 : !x1
            ans[(curr+1)/2] = curr%2 ? 0 : 1;
        }
    }
    for (int i=1;i<=N;i++){
        printf("%d ", ans[i]);
    }
    


    return 0;
}