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

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

11280번: 2-SAT - 3

---

Solved By: 2-SAT, SCC

 

처음으로 풀어본 2-SAT 문제였습니다. 2-SAT에 대해서는 주말에 간단하게 정리할 예정이며 직전 포스팅에 공부했던 포스팅들의 링크를 걸어두었습니다.

 

변수와 NOT 변수에 대해서 {2 * i, 2 * i + 1}로 각각 모델링하여 SCC를 Tarjan Algorithm을 통해 만들었습니다.

각 변수들을 탐색하며 한 변수와 NOT 변수에 대해 같은 SCC에 존재한다면 이는 true로 만들 수 없는 식임을 출력해주었습니다.

 

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

vector<vector<int>> SCC;
vector<int> adj[MAX];
int visitedOrder[MAX];
int sccNum[MAX];
stack<int> s;
int order = 0, sccCnt = 0;
int n, m;

int dfs(int now){
    int parent = visitedOrder[now] = ++order;
    s.push(now);
    
    for(int i = 0; i < adj[now].size(); i++){
        int next = adj[now][i];
        
        if(visitedOrder[next] == -1){
            parent = min(parent, dfs(next));
        }
        else if(sccNum[next] == -1){
            parent = min(parent, visitedOrder[next]);
        }
    }
    
    if(visitedOrder[now] == parent){
        vector<int> scc;
        while(1){
            int temp = s.top(); s.pop();
            scc.push_back(temp);
            sccNum[temp] = sccCnt;
            if(temp == now) break;
        }
        
        SCC.push_back(scc);
        sccCnt++;
    }
    
    return parent;
}

void tarjan(){
    fill(visitedOrder, visitedOrder + MAX, -1);
    fill(sccNum, sccNum + MAX, -1);
    for(int i = 2; i <= 2 * n + 1; i++){
        if(visitedOrder[i] == -1) dfs(i);
    }
}

int main(){
    cin >> n >> m;
    for(int i = 0; i < m; i++){
        int a, b; cin >> a >> b;
        //a = 2 * i, NOT a = 2 * i + 1
        
        int not_a, not_b;
        if(a < 0){ // NOT
            a = -a;
            a *= 2; a++;
            not_a = a - 1;
        }
        else{
            a *= 2;
            not_a = a + 1;
        }
        
        if(b < 0){
            b = -b;
            b *= 2; b++;
            not_b = b - 1;
        }
        else{
            b *= 2;
            not_b = b + 1;
        }
        
        adj[not_a].push_back(b);
        adj[not_b].push_back(a);
    }
    
    tarjan();
    
    bool flag = 1;
    for(int i = 2; i <= 2 * n; i += 2){
        if(sccNum[i] == sccNum[i + 1]){
            flag = 0; break;
        }
    }
    
    if(flag == 1) cout << 1;
    else cout << 0;
    
    return 0;
}