2-CNF Satisfiability Problem

2-satisfiability 문제. 2-SAT 으로 많이 쓰고, 읽을 때에는 '투셋' 정도로 부릅니다.

문제

n$n$개의 boolean variable X_0, X_2, \cdots, X_{n-1}$X_0, X_2, \cdots, X_{n-1}$이 있고, 주어진 2-CNF 식의 진리값을 true로 만들 수 있는 변수들의 assignment가 존재하는지를 판별하는 문제입니다. (혹은 있다면, valid한 assignment를 구함).

2-CNF 식이란

$$(x_0 \vee \lnot x_1) \wedge (\lnot x_2 \vee x_3)$$

처럼, 각각의 clause는 최대 두 개의 term (x_i$x_i$ 또는 \lnot x_i$\lnot x_i$ 꼴)의 disjunction(logical OR)으로 이루어지고, m$m$개의 clause들이 conjunction (logical AND)로 연결된 식을 말합니다. (TODO explain more formally)

해법

2-SAT 문제는 O(n+m)$O(n+m)$ linear time에 풀 수 있는 유명한 해법이 존재합니다.

그래프 구성

먼저 각 clause를 아래와 같이 해석합니다. 가령, (x_0 \vee \lnot x_1)$(x_0 \vee \lnot x_1)$ 이라는 clause가 있을 때, 이와 동치인 아래 조건

• \lnot x_0 \Rightarrow \lnot x_1$\lnot x_0 \Rightarrow \lnot x_1$
• \lnot (\lnot x_1) \Rightarrow x_0$\lnot (\lnot x_1) \Rightarrow x_0$ (i.e. x_1 \Rightarrow x_0$x_1 \Rightarrow x_0$)

으로 변환해서 생각합니다. (clause에 있는 두 term 중 한쪽의 값이 false이면, 다른 한 쪽의 값이 true여만 함은 자명합니다.)

이제 이런 조건들을 통해 implication graph를 구성합니다.

• 각 variable에 대해 두 개의 정점(x_i$x_i$, \lnot x_i$\lnot x_i$)을 구성합니다.
• p \Rightarrow q$p \Rightarrow q$ 라는 조건에 대해, 점 p$p$에서 q$q$로 directed edge를 그어줍니다.

$$\text{(TODO : 여기에 예시 그래프 그리기)}$$

직관적으로 p \Rightarrow q \Rightarrow r$p \Rightarrow q \Rightarrow r$이면, p$p$가 참이면 r$r$이므로 p$p$에서 r$r$로 이르는 path가 존재한다는 식으로 생각할 수 있습니다.

답이 존재하는가?

위 그래프에서, 어떤 variable x_i$x_i$에 대해 x_i \rightarrow \lnot x_i$x_i \rightarrow \lnot x_i$ 의 path와 \lnot x_i \rightarrow x_i$\lnot x_i \rightarrow x_i$ 의 path가 모두 존재한다면, 주어진 식은 unsatisfiable 입니다. 만약, 그런 variable이 하나도 없다면, 주어진 식은 satisfiable 입니다.
(latex 기호 \leadsto 가 안됨 ㅠㅠ)

직관적으로 생각해보면 당연한 게, 만약 x_i$x_i$를 가정했는데 \lnot x_i$\lnot x_i$가 추론된다면 모순이고, \lnot x_i$\lnot x_i$를 가정했는데 x_i$x_i$가 추론된다면 모순이므로 만족이 안 되겠죠. 그런데 역으로 이런 변수가 하나도 없다면 valid assignment가 존재한다는 것은 약간의 논리[..]가 필요합니다.

• 위의 조건을 검사하는 가장 (코딩이) 쉬운 방법은, floyd-warshall 알고리즘과 비슷한 O(n^3)$O(n^3)$ 루프를 돌려서 transitive closure를 구하는 겁니다. (i$i$에서 j$j$로 이르는 path가 있는지)
• 더 빠르게 하려면 : 먼저 강한 결합 요소 알고리즘을 돌려서 SCC C_1, C_2, ..., C_k$C_1, C_2, ..., C_k$를 구합니다. 그리고 x_i$x_i$와 \lnot x_i$\lnot x_i$가 같은 SCC에 존재하는지를 판별하면 됩니다. SCC는 O(V+E)$O(V+E)$에 구할 수 있으므로, 2-SAT 도 O(n+m)$O(n+m)$ 에 풀리겠죠.

Valid Assignment 찾기

이제 yes/no 를 판별하는 법을 알았습니다. 실제 많은 문제에서는 이정도 까지만 해도 충분한 경우가 많지만.. 경우에 따라 실제 주어진 식을 true로 만드는 변수들의 assignment 값을 구해야 할 필요가 있습니다. 아무거나 하나만 구해도 된다면 아래의 방법을 쓰면 됩니다.

(TODO)

문제 풀이 예시

이제 2-SAT 을 배웠으니, 이를 이용해서 실전 문제를 풀어보는 과정을 살펴보도록 하겠습니다. 실제로 2-SAT 문제는 방법 자체는 뻔하기(?) 때문에 구현하는 것 자체는 어렵지 않지만, 어떤 문제가 나왔을 때 이게 2-SAT인지 직관을 갖는 것과, 2-SAT 으로 풀릴수 있도록 변수와 식을 모델링하는 게 더 어렵습니다.

• (ICPC 한국대회 문제 간단히 설명)