2-SAT와 SCC (BOJ 11281)

2-SAT

$(a \vee b)$ $\wedge$ $(c \vee d)$ ..$\wedge$ $(\sim a \vee \sim b)$

같은 논리식을 만족시키는 진리표를 찾는것이 2-SAT 문제이다. 일반적으로 SAT문제는 NP군에 속하는 지수시간 복잡도를 갖는다. n개의 boolean 변수에 각각 true, false값을 배정해주는 경우의 수는 $2^n$임을 쉽게 알 수 있다. 하지만 2-SAT는 그래프로 모델링하여 scc를 통해 해결할 수 있다.

$a \vee b$ 논리식은
$\sim a > b$ , $\sim b > a$ 와 동치이다.

이 사실을 이용하면 각각의 UNION마다 두개의 간선을 도출해서 그래프로 모델링할 수 있다. 그리고 SCC로 분리하면, 각 SCC는 서로 같은 진리값을 (TRUE OR FALSE)를 가짐을 알 수 있다.

설명하기가 어려우니, 문제 하나를 직접 풀어보자.

구현

BOJ 11281

k번째 변수는 2k, 2k+1에 각각 참 거짓을 의미하는 정점을 배정했다.
scc 분류를 위해 sccId, order, 그리고 스택을 준비했다.

vi adj[MAX]; // (2,3) ~~ (2n, 2n+1) (+, -)
stack<int> st;
int sccId[MAX], order[MAX]; // memset to -1
int N, vcnt, scccnt;

void readInput() {
	int m;
    cin >> N >> m;
    for (int i = 0; i < m; ++i) {
        int a, b; cin >> a >> b;
        a = (a < 0) ? (-a) * 2 + 1 : 2 * a;
        b = (b < 0) ? (-b) * 2 + 1 : 2 * b;
		// ~a -> b, ~b -> a
        adj[(a % 2) ? a - 1 : a + 1].push_back(b);
        adj[(b % 2) ? b - 1 : b + 1].push_back(a);
    }
}
// scc 분류
int dfsScc(int here) {
    int ret = order[here] = vcnt++;
    st.push(here);

    for (int there : adj[here]) {
        if (order[there] == -1) 
            ret = min(ret, dfsScc(there));
        else if (sccId[there] == -1) 
            ret = min(ret, order[there]);
    }

    if (ret == order[here]) {
        while (true) {
            int temp = st.top(); st.pop();
            sccId[temp] = scccnt;
            if (temp == here) break;
        }
        scccnt++;
    }
    return ret;
}

이렇게 그래프 모델링 및, scc분류가 끝나고 나면 2-sat문제를 풀 준비가 완료된 것이다. 아래 함수는 각 정점의 진리값을 담은 배열을 리턴한다.

vi fun() {
    // Contradiction Check
    // i번째 변수에 대해서, i*2 정점은 i, i*2+1 정점은 ~i를 나타냄
    // 그 두 정점이 같은 scc에 속한다면 서로 같은 진리값을 가져야 함을 의미
    // 이는 명백히 모순이다.
    for (int i = 1; i <= N; ++i) {
        if (sccId[i * 2] == sccId[i * 2 + 1]) {
            return vi(); // 모순있으면 빈 배열 리턴
        }
    }

	// 모순이 없으므로 정답이 무조건 존재한다.
    // 아래 알고리즘이 바로 구성적 증명
    // 이 알고리즘이 찾아낸 정답이 모순이 없음을 증명할 수 있지만 생략
    vi ans(N + 1, -1); // 각 변수마다 할당되는 진리값 저장
    vector<pii> temp; //sccid 역순으로 정점 정렬, 위상정렬 성질 이용
    for (int i = 2; i <= 2 * N + 1; ++i) 
        temp.emplace_back(-sccId[i], i);
    sort(temp.begin(), temp.end());

    // 위상정렬 돼있으므로, 각 정점은 indeg가 0인 상태에서 방문됨
    // a->b에서 a가 먼저 방문된다는 뜻
    // 논리학적인 지식이 없으면 이해하기 어려울 수 있으나
    // a에 그냥 false를 할당해버리면 됨 (trivial하게 식을 만족시킴)
    // a에 false를 할당하면 ~a에는 true를 할당한 셈이다.
    for (pii& p : temp) {
        int v = p.second / 2, isTrue = p.second % 2 == 0;
        if (ans[v] != -1) continue; // 앞에서 ~v가 이미 할당됨
        ans[v] = 1-isTrue; //변수 v에 false를 할당(참이면 거짓, 거짓이면 참)
    }
    return ans;
}

관련문제

• BOJ 3648
  2-SAT + 1번 변수가 항상 참인 경우가 가능한지를 묻는 문제
  $a$ == $(a \vee a)$ == $(\sim a > a)$ ..?
• BOJ 2207