2-SAT 구하기

개요

2-SAT는 N개의 논리값을 가지는 변수를 사용하여 논리곱 정규형으로 표현했을 때, 각각의 절에 변수가 2개씩 존재하는 논리식을 의미합니다. 2-SAT는 기본적으로 아래와 같은 형식을 가지고 있습니다.

 

f = (~X₁ ∨ X₂) ∧ (~X₂ ∨ X₃) ∧ (X₁ ∨ X₃) ∧ (X₃ ∨ X₂)

 

이렇게 논리식 f를 참(true)로 만족하게 만드는 X₁ ~ X₃까지의 값을 구하는 것이 2-SAT 문제의 핵심입니다. 그럼 2-SAT의 값은 어떻게 구할 수 있을까요? 물론 X₁ ~ X₃까지 참(true)과 거짓(false)을 하나씩 넣어보는 브루트포스 방식으로 풀 수 있습니다. 그리고 2-SAT를 제외한 대부분의 CNF 문제(Ex. 3-SAT, 5-SAT)들은 NP-Hard문제로 브루트포스 방식으로 해결해야 합니다. 하지만 2-SAT는 2개의 변수만이 있다는 특수성 때문에 좀 더 빠르게 구할 수 있습니다. 그리고 그 때, SCC를 활용하게 됩니다.

 

방법

우선, 각각의 절을 분석해보아야 합니다. 논리식 f에서 가장 앞에 있는 (~X₁ ∨ X₂)을 예시로 살펴봅시다. (~X₁ ∨ X₂)가 참(true)를 만족하기 위해서는 다음과 같이 생각해볼 수 있습니다. 참고로, 논리식 f가 참(true)가 되기 위해서는 모든 절의 값이 참(true)이어야 합니다.

 

(1) 만약 ~X₁가 거짓이라면, X₂는 참이어야 한다. [ ~(~X₁) >> X₂ ]

(2) 만약 X₂가 거짓이라면, ~X₁는 참이어야 한다. [ ~X₂ >> (~X₁) ]

 

이렇게 2개의 명제가 만들어지며, 우리는 이 명제를 활용하여 그래프를 그려볼 수 있습니다. 그리고 이 그래프는 예상했겠지만 대칭을 이루게 됩니다. 이렇게 모든 절에 대해 명제를 2개씩 만들어보고, 이를 그래프로 표현하면 하나의 그래프를 만들 수 있습니다. 그리고 이 그래프를 분석하여 2-SAT를 구하면 됩니다.

 

우선, 논리식 f를 절대 참(true)으로 만들 수 없는 경우를 생각해봅시다. 이는 1개 이상의 명제에서 동일한 변수에 대해 참(true)와 거짓(false)이 연결되었다는 걸 의미합니다. 이를 그래프에 도입하면 X_n와 ~X_n이 서로 연결되었다는 걸 의미하며, 우리는 이를 그래프의 SCC를 구해보면 쉽게 파악할 수 있습니다. 그리고 SCC는 어떤 알고리즘(Kosaraju / Tajan)을 사용하든 동일한 시간 복잡도를 가지고 구할 수 있습니다.

 

만약, 직접 각각의 변수에 해당하는 값을 구해야 한다면 SCC가 만들어진 순서를 활용할 수 있습니다. SCC가 만들어진 순서는 곧 우리가 만든 논리식을 그래프로 표현했을 때, 위상 정렬되는 순서라고 할 수 있습니다. 그리고 위상 정렬되는 순서에 따라 나온 값을 거짓(false)으로 설정하면 우리가 원하는 결괏값을 얻을 수 있습니다. 아래 소스코드는 백준 11281번(2-SAT-4)번 문항(https://www.acmicpc.net/problem/11281)의 해결 소스코드입니다.

#include <stdio.h>
#include <string.h>
#include <stack>
#include <vector>
#include <utility>
#include <algorithm>
#define NMAX 20010
using namespace std;
typedef pair<int, int> PAIR;
 
int N, M, x, y;
vector< int > adj[NMAX], Radj[NMAX];
 
int top, sccIdx, f;
int visited[NMAX], sccNum[NMAX], ans[NMAX/2];
 
stack< int > st;
vector< PAIR > sccSort;
 
 
void dfs(int idx) {
    visited[idx] = 1;
    for(int nxt:adj[idx]) {
        if(!visited[nxt]) dfs(nxt);
    }
    
    st.push(idx);
}
 
void Rdfs(int idx) {
    visited[idx] = 1;
    for(int nxt:Radj[idx]) {
        if(!visited[nxt]) Rdfs(nxt);
    }
    
    sccNum[idx] = sccIdx;
    
    // 결괏값을 구하기 위해 sccIdx 순서로 저장
    sccSort.push_back({idx, sccIdx});
}
 
// Kosaraju's Algorithm
void getScc() {
    // 첫 번째 탐색
    for(int i=1*2;i<=N*2+1;i++) {
        if(!visited[i]) dfs(i);
    }
    
    // 두 번째 탐색 >> 역간선
    memset(visited, 0, sizeof(visited));
    while(!st.empty()) {
        top = st.top();
        st.pop();
        
        if(!visited[top]) {
            sccIdx++;
            
            // top과 동일한 SCC에 해당되는 정점 찾기
            Rdfs(top);
        }
        
    }
}
 
int main() {
    // 입력
    scanf("%d %d", &N, &M);
    for(int i=1;i<=M;i++) {
        scanf("%d %d", &x, &y);
        
        // true: idx*2 / false: idx*2+1
        x = x>0 ? x*2:(-x)*2+1;
        y = y>0 ? y*2:(-y)*2+1;
        
        // ~x > y
        if(x%2==0) {
            adj[x+1].push_back(y);
            Radj[y].push_back(x+1);
        }
        else {
            adj[x-1].push_back(y);
            Radj[y].push_back(x-1);
        }
        
        // ~y > x
        if(y%2==0) {
            adj[y+1].push_back(x);
            Radj[x].push_back(y+1);
        }
        else {
            adj[y-1].push_back(x);
            Radj[x].push_back(y-1);
        }
    }
    
    // SCC 구하기
    getScc();
    
    // 2-SAT를 구할 수 있는지 확인
    f = 1;
    for(int i=1;i<=N and f;i++) {
        if(sccNum[i*2] == sccNum[i*2+1]) f = 0;
    }
    
    if(!f) printf("0");
    else {
        printf("1\n");
        
        // SCC 순서대로 정렬하기 >> 낮을 수록 DAG에서 앞에 위치함
        // p > q에서 p가 false이면
        memset(ans, -1, sizeof(ans));
        for(PAIR p:sccSort) {
            int idx = p.first;
            
            // 현재 값을 거짓으로 설정
            if(ans[idx/2] == -1) ans[idx/2] = idx%2;
        }
        
        // 출력
        for(int i=1;i<=N;i++) printf("%d ", ans[i]);
        
    }
}