2-SAT

소프트웨어 수치해석 마지막 수정: 2026-08-28 04:47:41

1. 개요[편집]

2-SAT 2-satisfiability
입력	절마다 리터럴이 정확히 2개인 CNF
판정 복잡도	$O(n+m)$ — 선형
대비	3-SAT 은 NP-완전 (쿡-레빈)
핵심 정리	충족가능 ⟺ 어떤 $x$ 도 $x$ 와 $\lnot x$ 가 같은 SCC 에 없음
선형 알고리즘	아스프발-플라스-타잔(1979)
최적화판	MAX-2-SAT 은 다시 NP-난해
랜덤 상전이	절/변수 비 $\alpha = 1$ 에서 급변

2-SAT(2-satisfiability)은 모든 절이 리터럴 두 개의 논리합인 CNF 논리식이 참이 되게 하는 변수 배정이 있는지 판정하는 문제다. 예컨대 $(x_1 \vee \lnot x_2)\wedge(\lnot x_1 \vee x_3)\wedge(\lnot x_2 \vee \lnot x_3)$ 이 충족 가능한가를 묻는다.

이 문제가 유명한 이유는 순전히 경계선에 서 있기 때문이다. 절의 길이를 3 으로 늘린 3-SAT 은 쿡-레빈 정리 이래 NP-완전의 표준 대표선수이고, 절 길이를 2 로 줄이면 갑자기 선형 시간에 풀린다. 게다가 그 선형 알고리즘이 딱히 정교한 것도 아니고 강한 연결 요소를 한 번 구하는 게 전부다. “리터럴 하나 차이로 세상이 갈린다”는 계산 복잡도 이론의 대표적 절벽이며, 실무에서는 “내 제약을 2-SAT 으로 우겨넣을 수 있는가”가 곧 “다항시간에 풀리는가”의 판정 기준이 된다.

2. 왜 2 는 쉬운가 — 분해능 논증[편집]

SCC 이야기를 꺼내기 전에, 다항시간이라는 사실 자체는 훨씬 소박하게 나온다. 크롬(1967)의 논증이다.¹

절 두 개를 분해(resolution)하면 — $(a \vee b)$ 와 $(\lnot b \vee c)$ 에서 $(a \vee c)$ 를 얻는 그 규칙 — 2-절끼리 분해한 결과는 다시 2-절 이하다. 그런데 변수 $n$ 개로 만들 수 있는 서로 다른 2-절은 $O(n^2)$ 개뿐이므로, 분해를 더 이상 새 절이 안 나올 때까지 돌려도 $O(n^2)$ 번에 멈춘다. 빈 절이 나오면 충족 불가능, 안 나오면 가능이다. 끝.

3-SAT 에서 이 논증이 무너지는 지점이 정확히 보인다. 3-절끼리 분해하면 4-절이 나오고, 길이가 자라기 시작하면 가능한 절의 수가 $O(n^k)$ 로, 결국 지수로 폭발한다. 절 길이가 자라지 않는다는 닫힘 성질이 2 에서만 성립하는 것이 이 절벽의 정체다. 같은 이유로 호른 절(양의 리터럴이 최대 1개)도 다항시간이다 — 호른끼리 분해하면 호른이다.

3. 함의 그래프[편집]

크롬의 $O(n^2)$ 를 $O(n+m)$ 으로 끌어내리는 것이 함의 그래프다. 관찰은 하나다. 절 $(a \vee b)$ 는 함의 두 개와 논리적으로 동치다.

(a \vee b) \;\equiv\; (\lnot a \to b) \;\wedge\; (\lnot b \to a)

그러니 리터럴 $2n$ 개를 정점으로 삼고(변수마다 $x$ 와 $\lnot x$ 하나씩), 절마다 위 두 간선을 그으면 간선 $2m$ 개짜리 유향그래프 $G_\varphi$ 가 나온다. 단위절 $(a)$ 는 $(a \vee a)$ 로 보아 $\lnot a \to a$ 하나를 긋는다.

이 그래프에는 태생적인 대칭이 하나 있다. $u \to v$ 간선이 있으면 반드시 $\lnot v \to \lnot u$ 간선도 있다(대우). 따라서 리터럴을 부정으로 보내는 사상은 $G_\varphi$ 의 간선 방향을 뒤집는 반자기동형이고, SCC 를 SCC 로 옮기면서 축약 DAG 의 순서를 뒤집는다. 뒤에 나오는 모든 논증이 이 대칭 하나에 의존한다.

4. 아스프발-플라스-타잔 정리[편집]

정리 (Aspvall, Plass & Tarjan, 1979). $\varphi$ 가 충족 가능하다 $\iff$ 어떤 변수 $x$ 에 대해서도 $x$ 와 $\lnot x$ 가 $G_\varphi$ 의 같은 SCC 에 속하지 않는다.²

( $\Rightarrow$ 의 대우) $x$ 와 $\lnot x$ 가 같은 SCC 라면 $x \rightsquigarrow \lnot x$ 와 $\lnot x \rightsquigarrow x$ 경로가 둘 다 있다. 함의 경로는 “앞이 참이면 뒤도 참”을 뜻하므로, $x$ 를 참으로 두면 $\lnot x$ 도 참이어야 하고 거짓으로 두면 $x$ 가 참이어야 한다. 양쪽 다 모순이니 충족 불가능.

( $\Leftarrow$ ) 조건이 성립하면 해를 구성해서 보인다. 축약 DAG 의 위상 순서를 $t(\cdot)$ 라 할 때

x := \text{참} \iff t\bigl(\mathrm{comp}(x)\bigr) \;>\; t\bigl(\mathrm{comp}(\lnot x)\bigr)

즉 위상 순서에서 더 뒤(싱크 쪽)에 있는 리터럴을 참으로 둔다. 이 배정이 어떤 함의도 어기지 않음을 보이면 된다. 간선 $\ell \to m$ 이 있고 $\ell$ 이 참이라 하자. 간선이 있으므로 $t(\mathrm{comp}(\ell)) \le t(\mathrm{comp}(m))$ 이고, 대칭성으로 $\lnot m \to \lnot \ell$ 도 있으므로 $t(\mathrm{comp}(\lnot m)) \le t(\mathrm{comp}(\lnot \ell))$ 이다. $\ell$ 이 참이라는 것은 $t(\mathrm{comp}(\lnot \ell)) < t(\mathrm{comp}(\ell))$ 이므로 셋을 이으면

t(\mathrm{comp}(\lnot m)) \;\le\; t(\mathrm{comp}(\lnot \ell)) \;<\; t(\mathrm{comp}(\ell)) \;\le\; t(\mathrm{comp}(m))

이라 $m$ 도 참이다. 참인 리터럴이 거짓인 리터럴을 함의하는 일이 없으므로 모든 절이 만족된다. $\blacksquare$

증명이 알고리즘을 통째로 담고 있다는 점이 이 정리의 미덕이다. SCC 한 번 → 판정 → 해 구성이 전부이고 총 $O(n+m)$ 이다. 선형 시간 2-SAT 자체는 에벤·이타이·샤미르(1976)가 다른 방식으로 먼저 얻었지만, 지금 모두가 짜는 코드는 SCC 판이다.

구현에서 반드시 짚어야 할 함정이 하나 있다. 타잔 알고리즘은 SCC 를 역위상 순서로 번호 매긴다. 그래서 타잔을 쓰면 판정식이 comp[x] < comp[¬x] 로 뒤집힌다. 코사라주를 쓰면 위상 순서라 comp[x] > comp[¬x] 가 맞다. 부등호를 반대로 쓴 코드는 여전히 “충족 가능”이라고 답하고 배정도 뱉지만 그 배정이 절을 어긴다 — 판정은 맞고 해만 틀리는 유형이라 테스트가 얕으면 안 잡힌다. 답을 만들었으면 절을 다시 대입해 검산하는 습관이 국룰인 이유다.³

5. 어디에 쓰나[편집]

“둘 중 하나” 제약이 있는 스케줄링. 각 작업이 두 개의 슬롯(주간/야간, 라인 A/B) 중 하나를 골라야 하고 제약이 전부 쌍 단위 배제 — ” $i$ 가 A 면 $j$ 는 A 가 아니다” — 로 표현되면 그대로 2-SAT 이다. 선택지가 셋 이상이 되는 순간 그래프 색칠이 되며 NP-완전으로 넘어간다는 대비가 선명하다.

지도 라벨 배치. 지점마다 라벨을 두 위치 중 하나에 놓되 라벨끼리 겹치면 안 된다는 문제는 겹침 쌍마다 절을 하나 쓰는 2-SAT 이다. 포어만과 바그너(1991)는 여기에 “라벨 크기”를 이진 탐색으로 얹어 라벨 크기를 최대화하는 2-근사를 얻었다. 판정만 되면 최적화가 이진 탐색으로 따라온다는 이 패턴은 근사 알고리즘 설계의 정석이다.

이진 라벨링의 경성 제약. 픽셀·복셀마다 0/1 을 배정하는데 이웃 쌍에 반드시 지켜야 하는 제약이 걸려 있다면 그 실현 가능성 판정이 2-SAT 이다. 여기서 제약을 “어기면 벌점”인 연성 제약으로 바꾸면 문제가 그래프 컷 최소절단으로 옮겨가고(마르코프 확률장 에너지 최소화), 그 최소절단 그래프가 리터럴 $x$ 와 $\lnot x$ 를 정점으로 쓰는 QPBO 형태라 함의 그래프와 골격이 그대로 닮아 있다. 경성 제약이면 2-SAT, 연성이면 최소절단 — 같은 그림의 두 판본이다.

기하·메시의 방향 일관성. 삼각형 하나하나에 “뒤집는다/그대로 둔다”를 배정해 메시 생성 결과의 법선 방향을 맞추는 문제는, 공유하는 모서리마다 “정확히 하나만 뒤집혀야 한다”는 XOR 제약이 붙는다. $a \oplus b$ 는 $(a \vee b) \wedge (\lnot a \vee \lnot b)$ 로 2-CNF 이므로 2-SAT 이다. 물론 XOR 만 있는 특수 경우라 실제로는 GF(2) 위 선형 방정식이거나 2-색칠이고, 그래서 그냥 BFS 로도 풀린다 — 2-SAT 은 이 소박한 사실의 일반화다.

SAT 풀이기 내부. 실전 SAT 풀이기의 전처리 단계는 2-절만 모아 함의 그래프를 만들고 SCC 를 구한다. 같은 SCC 안의 리터럴들은 논리적으로 동치이므로 하나로 합쳐 변수 수를 줄이는데(equivalent literal substitution), 산업용 인스턴스에서 변수의 수십 퍼센트가 이렇게 날아가는 일이 흔하다. 주어진 CNF 를 변수 이름 바꾸기로 호른 형태로 만들 수 있는지 판정하는 문제(renamable Horn) 역시 2-SAT 으로 환원된다.

6. 랜덤 2-SAT 과 상전이[편집]

변수 $n$ 개에서 2-절을 무작위로 $m = \alpha n$ 개 뽑았을 때, $n \to \infty$ 에서 충족 가능할 확률이 $\alpha$ 를 기준으로 급격히 0 과 1 로 갈린다.

\alpha < 1 \Rightarrow \Pr[\text{충족 가능}] \to 1, \qquad \alpha > 1 \Rightarrow \Pr[\text{충족 가능}] \to 0

임계값이 정확히 $\alpha_c = 1$ 이라는 것이 1990년대 초에 증명됐고, $\alpha = 1$ 근방의 스케일링 윈도가 폭 $n^{-1/3}$ 짜리라는 정밀한 결과까지 나와 있다.⁴

임계값이 하필 1 인 것은 우연이 아니다. 절 하나가 함의 간선 두 개를 만들므로 리터럴 $2n$ 개짜리 함의 그래프의 평균 진출차수가 대략 $\alpha$ 이고, 랜덤 유향그래프는 평균 차수가 1 을 넘는 순간 거대 강연결 성분이 생긴다. 거대 SCC 가 생기면 어떤 변수의 $x$ 와 $\lnot x$ 가 그 안에 함께 빨려 들어갈 확률이 1 로 가고, 그게 곧 충족 불가능이다. 즉 2-SAT 의 상전이는 퍼콜레이션·에르되시-레니 랜덤 그래프의 거대 성분 출현과 같은 사건이다. 상전이 문서에서 다루는 임계 지수 언어가 여기 그대로 얹힌다.

3-SAT 도 비슷한 상전이를 보이지만 임계값이 $\alpha_c \approx 4.267$ 로 수치적으로만 알려져 있고, 임계점 근처에서 풀이 난이도가 폭증하는 “easy-hard-easy” 패턴이 나타난다. 2-SAT 에는 그런 난이도 봉우리가 없다 — 어차피 어디서든 선형 시간이다. 상전이는 있는데 계산적 난이도의 봉우리는 없다는 이 대비가 “물리적 상전이 = 계산적 난이도”라는 순진한 등식을 깨는 반례로 자주 인용된다.

7. MAX-2-SAT 이라는 배신[편집]

“판정이 선형이니 최적화도 쉽겠지”는 틀렸다. 최대한 많은 절을 만족시키는 MAX-2-SAT 은 판정판이 NP-완전이고 최적화판은 NP-난해다(게리·존슨·스톡마이어, 1976). 심지어 APX-난해라 PTAS 도 없다. 반정부호 계획 완화로 0.94 언저리의 근사비가 알려져 있는 정도다.⁵

이 대비는 되새길 만하다. 2-SAT 은 “모든 절”이라는 전칭 조건 덕분에 함의라는 전파 가능한 국소 구조를 얻는다. 절 하나를 포기해도 된다고 허용하는 순간 그 전파가 끊기고, 어느 절을 버릴지 고르는 조합 폭발이 되살아난다. 같은 이유로 2-SAT 인스턴스에 변수별 비용을 붙여 “참인 변수 수를 최소화”하는 문제도 NP-난해다. 판정과 최적화 사이의 이 절벽은 조합 최적화 전반에서 반복되는 주제이고, 실무에서는 “제약은 2-SAT 으로 두고 목적함수는 정수계획법이나 국소 탐색에 넘긴다”는 하이브리드로 타협한다.

8. 관련 문서[편집]

Krom, M. R. (1967). “The decision problem for a class of first-order formulas in which all disjunctions are binary”. Zeitschrift für math. Logik 13, 15–20. 제목만 봐서는 SAT 논문인지 알 수 없는데, 사실 저자의 관심사는 1차 논리의 결정 문제였고 2-SAT 은 부산물이었다. 알고리즘 커뮤니티가 이걸 발굴한 건 한참 뒤다. ↩
Aspvall, B., Plass, M. F. & Tarjan, R. E. (1979). “A linear-time algorithm for testing the truth of certain quantified Boolean formulas”. Inf. Process. Lett. 8(3), 121–123. 세 쪽짜리다. 참고로 원 논문은 2-SAT 보다 넓은 문제(한정사가 붙은 2-CNF)를 다루고 있고, 우리가 아는 2-SAT 은 한정사가 전부 존재한정사인 특수 사례다. ↩
여담이지만 2-SAT 은 판정 문제로서 NL-완전이다. 즉 비결정론적 로그 공간이면 충분하고, 이머만-셀레페니 정리로 NL = coNL 이므로 충족 불가능 판정도 같은 자원으로 된다. 선형 시간이라는 사실보다 이쪽이 더 강한 진술인데, 정작 코드로 옮길 때는 아무 도움이 안 된다. 이론의 흔한 팔자다. ↩
Chvátal, V. & Reed, B. (1992) 및 Goerdt, A. (1996)가 임계값 1 을 확립했고, Bollobás, Borgs, Chayes, Kim & Wilson (2001)이 폭 $n^{-1/3}$ 의 스케일링 윈도를 규명했다. 통계물리에서 유한 크기 스케일링이라 부르는 것과 정확히 같은 형식이라, 논문에 임계 지수가 그냥 등장한다. 조합론과 통계역학이 같은 언어로 말하는 몇 안 되는 자리 중 하나. ↩
Garey, M. R., Johnson, D. S. & Stockmeyer, L. (1976)이 MAX-2-SAT 의 NP-완전성을 보였고, 괴만스-윌리엄슨의 반정부호 완화(MAX-CUT 에서 0.878)를 다듬은 Lewin, Livnat & Zwick (2002)이 MAX-2-SAT 에서 0.94 대의 근사비를 얻었다. “판정은 선형인데 최적화는 SDP 를 꺼내야 한다”는 문장이 이 문제의 성격을 다 말해 준다. ↩