[BOJ/11280] 2-SAT - 3, c++

🔗 링크

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

11280번: 2-SAT - 3

🤯 한줄 후기

그만 괴롭혀주라 2-SAT 이녀석

🤷 문제

👩‍💻 풀이

2-SAT 알고리즘 기본 문제

SCC 를 구할 때는 코사라주 알고리즘을 사용하였다.

 

먼저 k-SAT 이란 Satisfiability Problem 으로 충족 가능성 문제의 한 종류이다. 이는 k개의 변수와 OR 논리식으로 이뤄진 식에서 해당 식이 true 인지 false 인지를 찾아내고, true 일때 이를 만족시키는 각 변수의 값들을 알아내는 문제이다.

이 중 대체로 2-SAT 문제가 자주 보일텐데 그 이유는 1-SAT은 너무 쉽고 (ex. A^!B^C) 3-SAT 부터는 아직까지 다항시간 내에 풀 수 있는지 알 수 없는 P = NP 문제기 때문이다.

2-SAT은 선형시간 안에 해결 가능하다. 그래프를 만들어서 풀어줄 것이다.

각 변수별로 2개의 정점을 만들어주는데 A, !A 이렇게 정점, not을 붙인 정점 2개로 만들어준다.

자 이제, (A v B) 를 보면 이 논리식이 참이 되기 위해서는 A 가 false 일 경우 B 가 true 여야 하고, 반대로 B가 false일 경우 A가 true여야 한다.

즉, 그래프로 만들 때, !A -> B, !B -> A 간선을 만들어 주는 것이다.

이렇게 그래프를 만들고 나서 전체 논리식이 참인지 거짓인지 알아내는 방법은 SCC 알고리즘을 사용하면 된다고 알려져있다.

A 와 !A 가 같은 SCC 안에 속하지 않는다면 참. A, !A가 같은 SCC 라는 말은 즉, A -> !A, !A -> A와 같은 의미! 이는 A와 !A가 모두 참이란 말이니까 불가능한 말이다.

따라서 코드로 구현할 때, 그래프를 만들어 주고, 코사라주나 타잔 알고리즘을 사용하여 SCC 를 구한 후, 비교해보면 된다.

!A는 여기선 음수로 주어지기 때문에 배열에 넣을 수 있게끔 조정이 필요하다. 

💻 코드

//AC
//BOJ 11280 2-SAT 3
#include <iostream>
#include <vector>
#include <algorithm>
#include <cstring>
#include <stack>
using namespace std;
vector<vector<int>> graph;
vector<vector<int>> re_graph;
vector<int> scc;
stack<int> s;
bool visit[20005];
void dfs(int x) {
    visit[x] = true;
    for(int next : graph[x]) {
        if(!visit[next]) {
            dfs(next);
        }
    }
    s.push(x);
}
void re_dfs(int x, int y){
    visit[x] = true;
    scc[x] = y;
    for(int next : re_graph[x]) {
        if(!visit[next]) {
            re_dfs(next, y);
        }
    }
}
int re(int x, int N) {
    return x > N ? x - N : x + N;
}
int main(){
    ios_base::sync_with_stdio(false);   cin.tie(0);     cout.tie(0);
    int N, M;
    cin >> N >> M;
    graph.resize(2*N+5);
    re_graph.resize(2*N+5);
    scc.resize(2*N + 5);
    for(int i=0; i<M; i++) {
        int u, v;
        cin >> u >> v;
        if(u < 0)   u = -u + N;
        if(v < 0)   v = -v + N;
        graph[re(u, N)].push_back(v);
        graph[re(v, N)].push_back(u);
        re_graph[u].push_back(re(v, N));
        re_graph[v].push_back(re(u, N));
    }
    for(int i=1; i<=2*N+1; i++) {
        if(!visit[i])   dfs(i);
    }
    memset(visit, false, sizeof(visit));
    int idx = 1;
    while(!s.empty()) {
        int x = s.top();
        s.pop();
        if(!visit[x]) {
            re_dfs(x, idx++);
        }
    }
    for(int i=1; i<=N; i++) {
        if(scc[i] == scc[i+N]) {
            cout << 0 << '\n';
            return 0;
        }
    }
    cout << 1 << '\n';
    return 0;
}

참고

1. ICPC Sinchon 알고리즘 캠프 - 중급 스터디 '2-SAT' 강의

2.

https://justicehui.github.io/hard-algorithm/2019/05/17/2SAT/

[그래프] 2-SAT문제 - 1