Algorithm in A..Z - 2-SAT

개념

충족 가능성 문제 중 하나로써 아래와 같은 형태를 2-SAT 문제라 한다.

* 충족 가능성 문제 : Boolean으로 이루어진 식이 있을 때 해당 식이 True인 경우를 찾는 문제

f=(¬x1∨x2)∧(¬x2∨x3)∧(x1∨x3)∧(x3∨x2) 인 경우에 f를 true로 만드는 경우
¬ : NOT
∨ : OR
∧ : AND

 

괄호 안의 OR 연산으로 이루어진 것을 절(Clause)이라고 표현하고 AND와 절로 이루어진 식을 CNF(Conjunctive Normal Form)라고 한다.

 

각 절의 변수의 개수가 2개면 2-SAT이라 하고 N개면 N-SAT이라고 한다. 2개 같은 경우 SCC 알고리즘을 사용하여 쉽게 해결할 수 있지만, 3개 이상의 SAT 문제에서는 NP-Hard 문제이다.

---

작동원리

1. 각 절을 바탕으로 그래프를 작성한다.

(x1∨x2) 절이 있을 때 x1이 False면 x2는 True인게 자명하다. (x2가 False면 x1이 True인 것도 자명하다.)

각 변수와 NOT인 변수를 정점으로 보고 ¬x1→x2, ¬x2→x1의 명제를 간선으로 생각하여 그래프를 작성한다.

 

2. SCC 알고리즘을 사용하여 SCC를 구한다.

 

3. x와 ¬x이 같은 SCC에 있는 경우 2-SAT을 해결할 수 없다. (¬x⇒x은 모순이기 때문에)

 

4. 해결할 수 있는 경우 x의 SCC 번호가 ¬x의 번호보다 작은 경우 x는 True이다.

---

특징

p → q라는 명제가 있을 때

1) p가 참이면 q는 무조건 참이여야 한다.

2) p가 거짓이면 q는 참, 거짓 상관없다.

=> 각 변수들의 참, 거짓을 알고 싶을 때 위상 정렬을 진행한 후 방문하지 않은 정점에 False를 우선으로 대입하면서 변수들의 참, 거짓을 알 수 있다.

 

하나의 SCC 안에 속한 변수들은 모두 연속적으로 방문되므로 항상 같은 값으로만 설정될 겁니다.

---

시간 복잡도

1. SCC 알고리즘을 사용할 때 O(V + E)

 

O(V + E)

---

문제

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

11281번: 2-SAT - 4

---

코드

#include <bits/stdc++.h>
using namespace std;

constexpr int NONE = -1;

int n, m;
vector<vector<int>> graph;

inline int convert(int value) {
    return value <= n ? value + n : value - n;
}

int order;
stack<int> st;
vector<int> sccNumber, isVisited;
vector<vector<int>> scc;
int dfs(int index) {
    st.push(index);
    isVisited[index] = order++;

    int value = isVisited[index];
    for (auto &next : graph[index]) {
        if (isVisited[next] == NONE) {
            value = min(value, dfs(next));
        } else if (sccNumber[next] == NONE) {
            value = min(value, isVisited[next]);
        }
    }

    if (value == isVisited[index]) {
        vector<int> cycle;
        while (!st.empty()) {
            int i = st.top(); st.pop();

            cycle.push_back(i);
            sccNumber[i] = (int)scc.size();
            if (i == index) {
                break;
            }
        }

        scc.push_back(cycle);
    }

    return value;
}

int main() {
    ios::sync_with_stdio(false); cin.tie(nullptr); cout.tie(nullptr);

    cin >> n >> m;
    graph.resize(2*n + 1);
    sccNumber.resize(2*n + 1, NONE);
    isVisited.resize(2*n + 1, NONE);
    while (m--) {
        int s, e;
        cin >> s >> e;

        s = s < 0 ? convert(-s) : s;
        e = e < 0 ? convert(-e) : e;

        graph[s].push_back(convert(e));
        graph[e].push_back(convert(s));
    }

    for (int i = 1;i <= 2*n;++i) {
        if (isVisited[i] == NONE) {
            dfs(i);
        }
    }

    for (int i = 1;i <= n;++i) {
        if (sccNumber[i] == sccNumber[convert(i)]) {
            cout << 0 << "\n";
            return 0;
        }
    }

    cout << 1 << "\n";
    for (int i = 1;i <= n;++i) {
        cout << (sccNumber[i] >= sccNumber[convert(i)]) << " ";
    }
}