2-SAT

2-CNF Satisfiability Problem

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

문제

n개의 boolean variable 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 또는 \lnot x_i 꼴)의 disjunction(logical OR)으로 이루어지고, m개의 clause들이 conjunction (logical AND)로 연결된 식을 말합니다. (TODO explain more formally)

해법

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

그래프 구성

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

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

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

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

  • 각 variable에 대해 두 개의 정점(x_i, \lnot x_i)을 구성합니다.
  • p \Rightarrow q 라는 조건에 대해, 점 p에서 q로 directed edge를 그어줍니다.
\text{(TODO : 여기에 예시 그래프 그리기)}

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

답이 존재하는가?

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

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

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

Valid Assignment 찾기

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

(TODO)

문제 풀이 예시

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

  • (ICPC 한국대회 문제 간단히 설명)
3개의 댓글이 있습니다.
  • Soboru
    Soboru

    안녕하세요? 궁금한게 있습니다. ¬ 이 기호는 무슨 의미인가요?


    2년 전 link
  • astein
    astein

    not 을 의미합니다 :)


    2년 전 link
  • Soboru
    Soboru

    감사합니다.


    2년 전 link
  • 댓글을 남기시려면 로그인하세요.