2-SAT

2-SAT 문제

각 변수가 참/거짓 둘 중 하나이고, 절(clause)이 모두 변수 두 개의 OR로 이뤄진
논리식이 있다. 이 식 전체를 참으로 만드는 변수 배정이 존재하는지, 있다면 하나를
구하는 문제가 2-SAT이다. 일반 SAT는 NP-완전이지만, 절이 2개의 리터럴로만
이뤄지면 다항 시간에 풀린다.

핵심: OR를 함의로

\((a \lor b)\)는 다음 두 함의와 논리적으로 동치다.

$$ (a \lor b) \equiv (\lnot a \to b) \land (\lnot b \to a) $$

"\(a\)가 거짓이면 \(b\)는 반드시 참이어야 한다"는 뜻이다. 모든 절을 이렇게 함의 쌍
으로 바꿔, 각 리터럴(변수 \(x\)와 그 부정 \(\lnot x\))을 정점으로 하는 함의
그래프(implication graph) 를 만든다. 정점은 변수당 2개라 총 \(2n\)개다.

SCC로 모순 판정

함의 그래프에서 \(a \to b\) 경로가 있으면 "\(a\)가 참이면 \(b\)도 참"이라는 강제
관계가 성립한다. 따라서 어떤 변수 \(x\)에 대해 \(x\)와 \(\lnot x\)가 같은 SCC에
속한다면, \(x \to \lnot x \to x\)가 되어 "\(x\)가 참이면 \(x\)가 거짓이고, 거짓이면
참"이라는 모순이 생긴다.

판정 정리: 모든 변수 \(x\)에 대해 \(x\)와 \(\lnot x\)가 서로 다른 SCC에 있으면,
그리고 오직 그럴 때만 만족 가능한 배정이 존재한다.

이 정리 덕분에 2-SAT은 SCC 한 번으로 해결된다.

값 배정: 위상 순서

해가 존재할 때 실제 배정은 SCC의 위상 순서로 정한다. 타잔으로 SCC를 구하면
SCC 번호가 위상 역순으로 매겨지는데, 이때 규칙은 간단하다.

변수 \(x\)에 대해, \(x\)가 속한 SCC의 위상 순서가 \(\lnot x\)의 SCC보다 뒤에
있으면 \(x = \text{참}\), 아니면 거짓.

타잔의 comp 번호로 말하면 comp[x] < comp[¬x]일 때 \(x\)를 참으로 둔다(타잔
번호가 위상 역순이므로). 이 배정이 모든 함의를 어기지 않음은, 함의 그래프가
대칭(스큐 대칭) 구조를 갖기 때문에 보장된다.

복잡도

함의 그래프의 정점은 \(2n\)개, 간선은 절 하나당 2개이므로 \(2m\)개다. SCC가
\(O(V + E) = O(n + m)\)이므로 2-SAT 전체가 선형 시간에 끝난다.

정점 번호 매기기

변수 \(i\) (\(0 \le i < n\))에 대해 참 리터럴과 거짓 리터럴에 정점 번호를 부여한다.
흔한 방식은 정점 \(2i\)를 "\(x_i\) 참", \(2i+1\)을 "\(x_i\) 거짓"으로 두는 것이다.
그러면 리터럴 \(v\)의 부정은 v ^ 1로 간단히 얻는다.

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

int n, m;                 // 변수 수, 절 수
vector<int> g[20002];     // 함의 그래프 (정점 2n개)
int disc[20002], low[20002], comp[20002];
bool on_stack[20002];
stack<int> stk;
int timer_cnt = 0, scc_cnt = 0;

int NOT(int v) { return v ^ 1; }   // 리터럴의 부정

// (a OR b) 추가: a,b는 이미 인코딩된 리터럴 정점 번호
void add_or(int a, int b) {
    g[NOT(a)].push_back(b);   // ¬a -> b
    g[NOT(b)].push_back(a);   // ¬b -> a
}

void dfs(int u) {
    disc[u] = low[u] = ++timer_cnt;
    stk.push(u); on_stack[u] = true;
    for (int v : g[u]) {
        if (!disc[v]) { dfs(v); low[u] = min(low[u], low[v]); }
        else if (on_stack[v]) low[u] = min(low[u], disc[v]);
    }
    if (low[u] == disc[u]) {
        scc_cnt++;
        while (true) {
            int x = stk.top(); stk.pop();
            on_stack[x] = false; comp[x] = scc_cnt;
            if (x == u) break;
        }
    }
}

int main() {
    // ... 입력으로 절을 받아 add_or 호출 ...
    for (int i = 0; i < 2 * n; i++) if (!disc[i]) dfs(i);
    for (int i = 0; i < n; i++)
        if (comp[2 * i] == comp[2 * i + 1]) { puts("0"); return 0; }
    puts("1");
    // 값 배정: comp 번호가 작을수록 위상상 뒤(타잔 역순)
    for (int i = 0; i < n; i++) {
        bool val = comp[2 * i] < comp[2 * i + 1];  // true면 x_i = 참
        printf("%d ", val ? 1 : 0);
    }
    return 0;
}

흔한 실수

• 함의 한 쪽만 추가 — \((a \lor b)\)는 두 개의 간선(\(\lnot a \to b\),
  \(\lnot b \to a\))을 모두 넣어야 한다. 한쪽만 넣으면 대칭이 깨져 오답이 난다.
• 1-indexed 변수 — 문제에서 변수가 1번부터면 인코딩 시 1을 빼서 0-indexed로
  맞추자. 부호로 참/거짓을 주는 입력은 별도 변환이 필요하다.
• 값 배정 방향 혼동 — 사용하는 SCC 알고리즘이 위상 순서를 정순으로 주는지
  역순으로 주는지에 따라 부등호 방향이 바뀐다. 타잔은 역순이다.

강제 조건 인코딩

이 인코딩 표만 익혀 두면 "각 정점에 색을 둘 중 하나로 칠하되 제약을 만족"하는
다양한 문제를 2-SAT으로 환원할 수 있다. 대표 응용으로는 좌표/구간의 배치
충돌 회피, 불 변수 제약 만족, 그리고 일부 구성(constructive) 문제가 있다.