[2-SAT] - BOJ_11280 : 2-SAT - 3

2023.05.15 - [PS] - [강한 연결 요소 SCC] - BOJ_2150 : Strongly Connected Component

[강한 연결 요소 SCC] - BOJ_2150 : Strongly Connected Component

저번 SCC 공부는 사실 이번 2-SAT 풀이를 위해서 진행했었다.

2-SAT 풀이를 보기전, SCC에 대한 기본 지식이 없다면 위 글을 먼저 읽어볼 것.

오늘 풀어볼 문제인, 백준 11280번이다.

일단 2-SAT에 대한 이해부터 해보자면, 먼저 CNF에 대해 알아야 한다.

❓CNF(Conjunctive Normal Form)란?

• 여러개의 논리(Boolean 변수)가 or 로 묶여있는 절(clause)들이 모두 and로 연결되어 있는 형태
• 이때 절(clause)에 들어있는 Bool변수 갯수의 최댓값을 k라 할 때 K-CNF라 칭함
  간단하게 CNF가 무엇인지 이해가 된다면, 이제 SAT에 대해 알아보겠습니다.

❓SAT(Satisfiability Problem)란?

• CNF 식의 값을 True로 만들 수 있는 논리 변수들의 값을 찾는 문제
  • 모든 clause들은 and로 묶여있으므로 모든 clause들의 값은 True이여야 한다
  • 각 clause들 속 논리 변수들은 or로 묶여있으므로 그 중 하나 이상만 True이면 된다                                              (반대로 모두 false만 아니면 됨 <- 이것이 중요!)
• 일반적으로 2-CNF식과 3-CNF식으로 모두 표현되므로 2-SAT문제, 3-SAT문제로 구분된다
• 3-SAT문제의 경우 쿡-레빈정리에 의해 NP-완전인 것이 밝혀짐.
  • 아무튼 알고리즘이 없음, 근사 알고리즘, SAT 솔버 등으로 해결해야 한다. 난 안해!!!
• 2-SAT문제의 경우 SCC로 해결이 가능

 

그렇다면 우리는 SCC를 할 수 있으니, 2-SAT을 풀 수 있는 것이다!

문제를 한 번 보자.

⚒️간선 만들기

우선 이 문제의 TC를 예시로 들어서 CNF 식을 만들어보겠다.

$$(!1 or 2) and (!2 or 3) and (1 or 3) and (3 or 2)$$ (이해를 쉽게 돕기 위해 and와 or과 not기호 !를 사용했다.)

위 식이 참이 되게 하는 변수들의 조합은 어떤 경우가 있을까? 

우선 각 절은 모두 참이 되어야하므로, 각 절을 뜯어 보자.

첫번째 절인 (!1 or 2) 의 경우엔, 1이 !1과 2가 모두 거짓일 경우에 답이 없어진다.

즉, !1이 거짓일 경우(1이 참일 경우)에는 2는 반드시 참이어야하고, 2가 거짓일 경우에는 !1은 반드시 참(1이 거짓)이 되어야한다.

이를 관계식으로 써보면, not 2 -> not 1 , 1 -> 2 이 두가지 관계식이 나온다.

나머지 절들도 같은 방식으로 풀이를 해줄 것인데, 이때 다음과 같은 로직을 사용할 수 있다.

-      +	+      +	+      -	-      -
T -> F	F -> T	F -> F	T -> F
F <- F	T <- F	T <- T	F <- T

여기까진 이해가 된다.

그렇다면 이걸 코드로 구현하는 방법은 뭐가 있을까??

여기서 바로 SCC를 활용하는 것이다.

우선 그를 위해선 각 변수들을 노드로 할당해주고, 해당 변수의 FALSE에 해당하는, 음의 변수 또한 노드로서

할당을 해주어야하는데, 이는 흔히 음수로 인덱싱하고 싶을 때 사용되는 테크닉이다.

ex) 1 2 3번 노드가 있을때, 이를 arr 배열 1~3번 idx에 할당할 경우, -1 -2 -3에 해당하는 노드는 arr 배열 4~6 idx에 할당하는 방식

 

💡SCC를 활용하여 2-sat을 푸는 방법

먼저 논리적으로 생각해보자. 우리는 변수들을 노드로서 표현을 하기로 했다.

그리고, 해당 변수간의 관계식을 유향 간선 그래프로서 표현할 것이다.

그렇다면 그래프로 표현을 했을 때, 예를 들어 이런 경우가 있을 것이다.

 

case 1:

A가 참이면, (not A)도 참이다. (우선 A의 노드번호를 1로, (not A)의 노드번호를 2로 가정한다.)

즉, 그래프 내에 1->2 의 유향 간선이 존재하는 것이다.

이 경우는 괜찮다. 왜냐? A가 false가 될 경우, 명제의 논리상 not A는 true가 되기 때문이다.

 

case 2:

(not A)가 참이면, A도 참이다. (우선 A의 노드번호를 1로, (not A)의 노드번호를 2로 가정한다.)

즉, 그래프 내에 2->1 의 유향 간선이 존재하는 것이다.

이 경우도 괜찮다. not A가 false가 될 경우, 명제의 논리상 A는 true가 되기 때문이다.

 

case 3:

A가 참이면, (not A)는 참이다. + (not A)가 참이면, A는 참이다.

1->2의 유향 간선도, 2->1의 유향 간선도 존재하는 것이다.

이 경우는 문제가 생긴다. 절대 가능할 수 없는 경우이기 때문이다. 

A가 false가 될 경우, not A는 true가 되지만(첫번째 조건), not A가 true라면 A또한 true여야 하므로(두번째 조건)

즉, A와 not A가 같은 SCC를 이루고 있는 경우이다.

 

case 3과 같은 모순이 CNF 내부에 존재하지 않는다면, 우리는 해를 구할 수 있다.

다시말해해 우리는 A와 not A가 같은 SCC에 있는지만 확인을 한다면, 해가 존재하는지의 여부를 확인할 수 있게 되었다.

 

간선은 SCC를 구할때 추가했듯이 하되, 위 간선 만들기에서 설명한 방식대로 진행한다.

이제 코드를 짜보며 진행해보자.

SCC 코드는 이전 SCC문제를 풀때 사용했던 코드를 재사용하였다.

 

📜CODE

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

int n,e;
vector<int> vertex[20'002];
int visited[20002];
int discover[20002];
stack<int> stk;
vector<vector<int>> scc;
int sequence[20002];
int t=1;
int num;
int sccNum[20002];


void addScc(int x);

int makeScc(int cur){ 
    discover[cur]=1;
    sequence[cur]=t++;          //방문 순서대로 id 발급
    int parent=sequence[cur];
    
    stk.push(cur);

    int Nnode;
    for(int i=0; i<vertex[cur].size(); i++){
        Nnode=vertex[cur][i];
        if(visited[Nnode]) continue;  //이미scc를 이룬 노드를 방문
        if(discover[Nnode]){   // 방문할 노드가 scc를 이루지 않았지만 이미 방문되었을때 (즉 사이클을 이룰때)
            parent=min(parent,sequence[Nnode]);     //부모를 해당 노드로 바꾸고 다시 자식 dfs 탐색
            continue;
        }
        parent=min(parent,makeScc(Nnode));   //가장 먼저 방문한 노드가 부모가 된다
    }

    if(parent==sequence[cur]){  //자식중에 나에게 돌아오는 노드가 없거나, 있을 때 모두 해당 즉, 내가 자식이 아닐 때
        addScc(cur);
    }
    
    return parent;
}

void addScc(int cur){
    num++;
    int tmp;
    while(true){
        tmp=stk.top();
        sccNum[tmp]=num;
        visited[tmp]=1; //현재 요소가 scc를 이룸
        stk.pop();
        if(tmp==cur){
            break;
        }
    }
    
    return;
}

int main(){
    cin.tie(0)->ios::sync_with_stdio(0);
    cin>>n>>e;

    int Pnode,Nnode;
    while(e--){
        cin>>Pnode>>Nnode;
        if(Pnode>0&&Nnode>0){
            vertex[Pnode+10000].push_back(Nnode);
            vertex[Nnode+10000].push_back(Pnode);
        }
        else if(Pnode<=0&&Nnode<=0){
            vertex[abs(Pnode)].push_back(abs(Nnode)+10000);
            vertex[abs(Nnode)].push_back(abs(Pnode)+10000);
        }
        else if(Pnode>0&&Nnode<=0){
            vertex[Pnode+10000].push_back(abs(Nnode)+10000);
            vertex[abs(Nnode)].push_back(Pnode);
        }
        else if(Pnode<=0&&Nnode>0){
            vertex[Nnode+10000].push_back(abs(Pnode)+10000);
            vertex[abs(Pnode)].push_back(Nnode);
        }
    }
    for(int i=1; i<=n; i++){
        if(!discover[i])
            makeScc(i);
    }

    for(int i=1; i<=n; i++){
        if(!discover[10000+i])
            makeScc(10000+i);
    }

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