기초 상식. 연언(conjunction)은 논리적 「AND」를 가리키는 「올바른」 용어입니다($\wedge$ 또는 &로 표기합니다). 연언은 두 변수가 모두 true일 때, 그리고 오직 그때에만 true를 반환합니다.
기초 상식. 디스정크션(disjunction)은 논리 “OR"를 가리키는 “정식” 용어입니다($\vee$ 또는 |로 표기합니다). 디스정크션은 두 변수가 모두 false일 때, 그리고 오직 그때에만 false를 반환합니다.
절(clause)들의 논리곱(conjunction), 즉 어떤 변수들 또는 그 부정들의 «OR»들에 대한 «AND»를 생각해 봅시다. 예를 들어, 다음과 같은 식입니다:
(a | b) & (!c | d) & (!a | !b)
글자로 쓰면 다음과 같습니다: (A OR B) AND (NOT C OR D) AND (NOT A OR NOT B).
모든 논리식을 이러한 형태로 나타낼 수 있음을 보일 수 있습니다.
충족 가능성 문제(satisfiability, SAT)는 식이 참이 되도록 하는 변수의 값을 찾거나, 그러한 값의 조합이 존재하지 않는다고 답하는 문제입니다. 위의 예에서는 a=1, b=0, c=0, d=1이 그러한 값입니다(각 괄호가 true가 되는지 확인해 보십시오).
임의의 식에 대해서는 이 문제를 빠르게 풀 수 없습니다. 우리는 이 문제의 특수한 경우, 즉 각 괄호에 정확히 두 개의 변수가 있는 경우(2-SAT)를 풀고자 합니다.
#함의 그래프
그런데 여기서 그래프가 무슨 상관일까요? 식 $a | b$는 $(!a \rightarrow b) | (!b \rightarrow a)$와 동치임에 주목하십시오. 여기서 «$\rightarrow$»는 함의(«$a$가 참이면 $b$도 참이다»)를 의미합니다. 이 치환을 이용하여 식을 다른 형태, 즉 함의 형태로 바꾸어 봅시다.
그다음 함의 그래프를 만듭시다. 그래프에는 각 변수마다 정점이 두 개씩 있으며(이를 $x$와 $!x$로 나타냅시다), 이 그래프의 간선은 함의에 대응합니다.
함의 그래프가 유용한 이유는 어떤 식을 참으로 정하면, 그 식으로부터 따라 나오는 모든 식, 즉 함의 그래프에서 도달 가능한 모든 식도 참으로 정해야 하기 때문입니다.
어떤 변수 $x$에 대해 $x$에서 $!x$에 도달할 수 있고 $!x$에서 $x$에 도달할 수 있다면, 문제의 해가 존재하지 않는다는 점에 주목합시다. 실제로 변수 $x$에 어떤 값을 선택하든, 그와 반대되는 값도 선택되어야 한다는 모순에 항상 도달하게 됩니다.
이 기준을 그래프 이론의 용어로 다시 표현해 봅시다. 한 정점에서 다른 정점에 도달할 수 있고 그 반대도 성립한다면, 이 두 정점은 같은 강한 연결 요소에 속합니다. 그러면 해가 존재하기 위한 조건은 다음과 같습니다. 2-SAT 문제가 해를 가지려면, 모든 변수 $x$에 대해 정점 $x$와 $!x$가 함의 그래프의 서로 다른 강한 연결 요소에 속해야 합니다.
이 조건은 필요조건일 뿐만 아니라 충분조건이기도 하다는 것이 밝혀집니다. 아래에 설명하는 알고리즘이 이 사실의 증명이 됩니다.
#2-SAT 해결 알고리즘
해가 존재한다고 가정하고, 그 해를 찾아야 한다고 합시다. 일부 변수에 대해서는 $x$에서 $!x$에 도달할 수 있거나 $!x$에서 $x$에 도달할 수 있는 경우(단, 동시에는 아님)가 있을 수 있다는 점에 주목하십시오. 이러한 경우 변수 $x$의 값 중 하나를 선택하면 모순이 발생하지만, 다른 하나를 선택하면 모순이 발생하지 않습니다. 두 값 중 모순을 일으키지 않는 값을 선택하려면 다음의 간단한 규칙을 사용할 수 있습니다.
규칙. $с[x]$를 정점 $x$가 속한 강한 연결 요소의 번호라고 하고, 이 번호들은 강한 연결 요소들의 위상 정렬 순서대로 매겨져 있다고 합시다. 즉 $x$에서 $y$로 가는 경로가 있으면 $c[x] \leq c[y]$입니다. 이때 $c[x] > c[!x]$이면 $x$를 선택하고, 그렇지 않으면 $!x$를 선택합니다.
이렇게 값을 선택하면 모순에 이르지 않음을 증명합시다. 구체적으로 $c[x] > c[!x]$이고, 그래서 정점 $x$가 선택되었다고 합시다($!x$의 경우도 증명은 같습니다).
- $x$에서 $!x$에 도달할 수 없음을 보이겠습니다. 강한 연결 요소의 번호 $c[ x ]$가 요소 $c[ !x ]$의 번호보다 크므로, $x$의 연결 요소는 $!x$의 연결 요소보다 “왼쪽"에 위치하며, 따라서 앞의 요소에서 뒤의 요소로는 결코 도달할 수 없습니다.
- $x$에서 도달 가능한 임의의 정점 $y$에서 $!y$에 도달할 수 없음을 보이겠습니다. 귀류법으로 증명합시다. $x$에서 $y$에 도달 가능하고, $y$에서 $!y$에 도달 가능하다고 가정합시다. 함의 그래프는 $(a | b) \leftrightarrow ((!a \rightarrow b) | (!b \rightarrow a))$ 변환으로 얻었고 $x$에서 $y$에 도달 가능하므로, $!y$에서 $!x$에 도달 가능합니다. 그런데 가정에 따라 $y$에서 $!y$에 도달 가능합니다. 그러면 $x$에서 $!x$에 도달 가능하게 되며, 이는 조건에 모순입니다.
결국 참으로 표시된 임의의 식에서 그 부정에는 도달할 수 없으며, 그로부터 도출되는 임의의 식들에서도 각각의 부정에는 도달할 수 없으므로, 이러한 규칙을 따르면 모순이 생기지 않습니다.
이렇게 해서 우리는 임의의 변수 $x$에 대해 정점 $x$와 $!x$가 서로 다른 강한 연결 요소에 속한다는 가정하에 구하려는 변수 값을 찾는 알고리즘을 만들었습니다:
- $a | b$ 형태의 모든 식을 두 간선 $!a \rightarrow b$와 $!b \rightarrow a$로 바꾸어 함의 그래프를 만듭시다.
- 함의 그래프에서 모든 강한 연결 요소를 찾습니다.
- 임의의 값 $x$에 대해 그 부정이 다른 강한 연결 요소에 속하는지, 즉 $c[ x ] \neq c[ !x ]$인지 확인합시다. 그렇지 않다면 해는 존재하지 않습니다.
- 답을 출력해야 하는 경우, $c[ x ] < c[ !x ]$이면 조건 $x$를 참으로 두고, 그렇지 않으면 거짓으로 둡니다.