2-SAT 연구일지

2-SAT에 대하여 공부해봅시다.

 

2-Satisfiability의 약자로 boolean variable들의 충족 가능성을 묻는 문제입니다.

 

BOJ 2-SAT 3(11280), 2-SAT 4(11281)를 기반으로 연구합니다.

 

공부하는 데에 도움이 된 블로그 링크들

1(https://blog.naver.com/kks227/220803009418)

2(https://everenew.tistory.com/140)

---

22.04.03 연구일지

CNF(Conjunctive Normal Form) 식을 true가 될 수 있게 boolean variable의 조합이 있는지 조합이 있다면 어떤 조합으로 이루어지는지 알아내는 알고리즘입니다.

2-SAT에서 CNF는 2-CNF로 이는 한 Clause당 boolean variable이 최대 2개가 있다는 뜻입니다.

 

한 Clause안에서 boolean variable들끼리는 OR연산(논리합)이 되어있으며 Clause끼리는 AND연산(논리곱)으로 이루어집니다.

f = (x1 | ~x2) & (x2 | ~x3) & (x3 | ~x1) & (~x4 | ~x2)

 

&연산에 의해 모든 Clause는 true값을 내놓아야 합니다.

즉, 2-SAT 문제는 각 Clause의 변수들 중 적어도 하나가 true가 되게 하는 것이 문제를 푸는 방향이 됩니다.

 

OR이 true가 되는 조건은

1) x1 = true, x2 = true

2) x1 = true, x2 = false

3) x1 = false, x2 = true

가 있습니다.

 

두 variable 중에 적어도 하나만 true를 내놓는다면?

논리합이기 때문에 두 변수 모두 다 true가 아니어도 됩니다.

즉, 이렇게 정리할 수 있습니다.

 

✔️2-SAT 핵심 아이디어(1): 각 Clause에서 true를 내놓으려면?

~x1 -> x2: x1이 false라면, x2가 true여야 한다.

~x2 -> x1: x2가 false라면, x1이 true여야 한다.

 

+ 논리학(Logics)에서도 위 내용은 논리적 동치라고 나와있습니다.

(p V q) ≡ (~ p -> q)

+ (p V q)는 교환 법칙이 성립함으로 (~q -> p)를 도출할 수 있습니다.

 

그러면 아까 위의 식에서 다음 true propostion 조건문들을 도출할 수 있습니다.

~x1 -> ~x2

x2 -> x1

~x2 -> ~x3

x3 -> x2

~x3 -> ~x1

x1 -> x3

x4 -> ~x2

x2 -> ~x4

 

이들을 삼단논법을 이용해서 추론하여 그래프로 나타낼 수 있습니다.

Skew-Symmatric Graph (반대칭 그래프)

다음과 같이 그래프로 나타내면 SCC가 형성되어있는 것을 확인할 수 있습니다. 

 

모순

✔️2-SAT 핵심 아이디어(2): 2-SAT이 성립하지 않는 순간, 모순

 

위 그림에는 없지만 추론하는 과정에서 같은 SCC안에 ~p와 p가 같이 들어있다면, 이건 모순을 의미합니다.

같은 SCC안에 들어있다는 것은 함축하였을 때, ~p -> p와 p -> ~p임을 의미하기 때문입니다.

 

둘 중 하나의 명제가 좌변이 false이고, 우변이 true라면 이는 성립하겠지만 그 반대는 성립하지 않기 때문에 모순입니다.

>> 이와 관련에서 무슨 말인지 밑에서 다루겠습니다. (명제 논리, 조건문)

 

즉, 모순이 없다면 식 f에서 true값을 가져올 수 있는 boolean variable의 조합이 있다는 뜻입니다.

 

명제 논리, 조건문

✔️2-SAT 핵심 아이디어(3): 명제 논리에 따른 조건문이 참 혹은 거짓이 되는 경우

명제 논리에 따르면 조건문은 아래 표와 같은 경우에서 참임을 의미합니다.

p	q	p -> q
T	F	F
F	F	T
T	T	T
F	T	T

p가 참일 때, q가 거짓인 경우를 제외하면 모든 경우에서 참입니다.

>> 즉, SCC를 구성하는 노드 중 하나라도 참이 있다면 해당 SCC는 모두 참이어야 합니다.

 

여기까지의 지식을 가지고서 2-SAT을 만족하는 조합이 있는지 없는지를 찾을 수 있습니다.

 

이를 코드로 표현하기 위해 모델링하려면

1. 각 Clause에서 두 가지 명제를 도출해낸다.
2. 도출해낸 명제들을 가지고, 그래프를 만든다.
3. 그래프에서 SCC를 구하고, 어떤 한 변수와 그 변수의 NOT 변수가 같은 SCC에 없다면 이는 성립함을 의미한다.

여기까지의 지식을 가지고서 2-SAT 3 (11280)을 풀 수 있습니다.

+변수에 대해서 변수 그 자체는 2를 곱하여 짝수로 나타내고, NOT 변수는 2를 곱하여 1을 더해주었습니다.

#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
        
        // 2가지 명제 도출 과정
        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;
}

여기까지 2-SAT이 성립하는지에 대하여 알아보았습니다.

 

✔️2-SAT 핵심 아이디어(4): 2-SAT이 성립한다면 변수들은 어떤 값인지 알 수 있을까?

 

만약 2-SAT이 성립한다면 각 boolean variable들은 어떤 값을 가져야 할까요?

위에서 말했듯이 SCC를 구성하는 변수들은 모두 같은 값을 가져야 합니다.

 

그렇게 되면 SCC를 노드 단위로 보면 됩니다.

아까 위의 그림을 다시 가져와서 보면, {x4} -> {~x1, ~x2, ~x3}로 가고 있습니다.

p	q	p -> q
T	F	F
F	F	T
T	T	T
F	T	T

이 표에 의거하여 x4를 false로 두는 것이 명제를 해치지 않기 때문에 좋습니다.

즉, 위상 정렬을 통해 처음 방문한 값들을 false로 두는 것이 좋습니다. ~x4도 indegree가 없기 때문에 ~x4를 false로 두어도 됩니다.

 

>> 변수 혹은 not 변수 중 먼저 방문하는 순서대로 false를 준다는 뜻입니다.

 

✔️2-SAT 핵심 아이디어(5): 위상 정렬을 통한 SCC끼리의 조건문

 

위상 정렬을 확인하는 방법은 Tarjan Algorithm의 특성으로 만들어진 순서를 반대로 뒤집으면 위상 정렬이 됩니다.

즉, SCC에 생긴 순서대로 번호를 매기고, 이를 내림차순으로 정렬하면 됩니다.

>> 이 아이디어에서 좀 놀랬습니다..

왜 위상 정렬이 되는지는 자세한 내용은 Tarjan Algortihm 연구일지를 참고하길 바랍니다.

(https://draw-code-boy.tistory.com/274)

 

+ 예를 들어, ~x1 -> x1의 경로가 있다면 이는 상관없습니다. 이미 ~x1을 방문하면서 ~x1은 false가 되었고, x1은 true가 되었기 때문입니다.

 

여기까지 내용을 인지하고, 코드로 모델링한다면

1. 각 Clause에서 두 가지 명제를 도출해낸다.
2. 도출해낸 명제들을 가지고, 그래프를 만든다.
3. 그래프에서 SCC를 구하고, 어떤 한 변수와 그 변수의 NOT 변수가 같은 SCC에 없다면 이는 성립함을 의미한다.
4. 성립한다면 각 변수가 어떤 값을 지니는지 알 수 있다.
5. 각 SCC를 하나의 노드로 보고, 위상 정렬에 의해 제일 늦게 만들어진 SCC를 순서로 노드를 방문하여 만나는 변수에 false값을 준다.

 

여기까지의 지식을 가지고서 2-SAT 4 (11281)을 풀 수 있습니다.

#include <iostream>
#include <vector>
#include <algorithm>
#include <stack>
#define MAX 20002
#define pii pair<int, int>
using namespace std;

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

bool cmp(pii a, pii b){
    return a.second > b.second;
}

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

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;
        
        int not_a, not_b;
        if(a < 0){
            a = -a; a *= 2; a += 1;
            not_a = a - 1;
        }
        else{
            a *= 2;
            not_a = a + 1;
        }
        
        if(b < 0){
            b = -b; b *= 2; b += 1;
            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){
        cout << 1 << '\n';
        vector<pii> satOrder;
        for(int i = 2; i <= 2 * n + 1; ++i){
            //{vertex || ~vertex, vertex's SCCnum}
            satOrder.push_back({i, sccNum[i]});
        }
        
        // SCC가 만들어진 순서를 내림차순으로 정렬해주었다.
        sort(satOrder.begin(), satOrder.end(), cmp);
        
        vector<int> answer(n + 1, -1);
        
        for(int i = 0; i < satOrder.size(); i++){
            int vertex = satOrder[i].first;
            int varIdx = vertex / 2;
            int isTrue = (vertex % 2 == 0);
            if(answer[varIdx] != -1) continue;
            
            // 처음 방문하는 변수에 true이면 false, false이면 true를 준다.
            answer[varIdx] = !isTrue;
        }
        
        for(int i = 1; i < answer.size(); i++){
            cout << answer[i] << ' ';
        }
    }
    else{
        cout << 0 << '\n';
    }
    return 0;
}

---

결론

여태껏 그래프 알고리즘만 공부하다가 논리학에 관련된 알고리즘을 공부하다 보니 시간을 들여야 했습니다. 물론, SCC를 활용하여 그래프 알고리즘이기도 하지만. 다른 영역의 알고리즘을 건드려야겠다는 생각이 부쩍 들었었는데 한 걸음 나아간 것 같습니다.

 

그리고, 반년 전쯤 알고리즘을 막 시작할 때, '2-SAT'이라는 이름이 멋져 보여서 저런 알고리즘은 엄청 어려울 거 같아서 언젠간 배우고 싶었는데 SCC를 공부하다 보니 자연스럽게 2-SAT을 건드리게 되어 기분이 오묘한 순간이었습니다.

 

아직은 미숙지 된 내용들에 대해 계속 추가적으로 수정하거나 구현을 해보며 익혀야겠습니다.