koosaga's profile image

koosaga

June 17, 2019 23:59

계산 복잡도 위계와 불리언 식

computation-theory , logic , algorithm

계산 복잡도 위계와 불리언 식

계산 이론은 전산학의 근간을 이루며, 컴퓨터를 사용하는 모든 학문의 수학적 분석에 있어서 중요한 역할을 한다. 계산 이론 분야의 $P = NP$ 난제는 컴퓨터 과학의 거의 모든 분야를 관통하는 중요한 문제이고. $P = NP$ 난제의 여러 중요한 실용적 의미와 그 악명높음은 이미 대중적으로도 잘 알려져 있다.

계산 이론의 내용은 전산학의 어떠한 부분을 다루더라도 만나게 되는 경우가 많지만, 대부분의 내용은 튜링 머신과 같은 복잡한 개념을 바탕으로 정의된다. 이러한 특징 때문에, 계산 이론의 많은 내용은 잘 알려져 있으면서도 제대로 알고 있는 사람은 그렇게 많지 않은 경우가 많다. NP 시간 복잡도가 Non-Polynomial의 줄임말이라는 유명한 오해가 대표적인 사례이다.

튜링 머신과 같은 개념은 매우 저수준의 개념이어서, 이러한 개념 하에서 엄격하게 계산 이론을 접근할 경우 일반적인 알고리즘 현상들을 설명하는 게 힘들어진다. 이 글에서는 가능 단순하고 일상적인 언어로 주요 시간 복잡도 클래스와 위계 (Hierarchy), 그리고 각 클래스의 가장 어려운 문제인 SAT / QBF 문제를 정확하게 설명하는 것을 목표로 한다. 또한, SAT / QBF 문제 중 효율적인 풀이가 가능한 특수한 케이스인, Horn Formula와 2-CNF에 대한 연구와 문제 해결 방법을 설명한다.

계산 모델

계산 이론에서 표준적으로 다루는 계산 모델은 튜링 머신 이라 불리며, 무한히 긴 테이프, 그리고 테이프에 문자를 덮어쓸 수 있는 머리, 각 상태에 대해서 머리가 움직여야 할 지 적어야 할 지를 나타내는 상태 표 등으로 구성되어 있다. 튜링 머신은 매우 저수준의 컴퓨터라고 할 수 있으며, 현실적인 알고리즘을 모델링 할 경우 굉장한 수준의 노동이 필요하다. 이 글의 범위에서 튜링 머신은 필요하지 않고, 대신 다음과 같은 간단한 연산을 지원하는 C 언어의 부분집합을 사용할 것이다.

  • 사칙연산, 비트 연산
  • 배열
  • 배정 (assignment)
  • while 문

각 연산의 시간 복잡도는 일반적인 C 언어와 동일하다고 가정한다. 이 언어는 튜링 머신이 할 수 있는 모든 것을 할 수 있으며, 실제 컴퓨터처럼 배열 접근을 $O(1)$ 에 할 수 있기 때문에 튜링 머신보다 효과적이다.

이 글에서는 모든 알고리즘 문제는 결정 문제 로 정의한다. 결정 문제 는 주어진 입력 $X$ 가 특정 조건을 만족하는지를 판별하는 문제라고 할 수 있다. 결정 문제는 $X$ 가 특정 조건을 만족하지 않는다면 $X$ 가 조건을 만족하지 않는다고 해야 하고, $X$ 가 조건을 만족한다면, 만족함과 동시에 조건을 만족한다는 증거 를 제시해야 한다.

일반적인 알고리즘 문제 해결을 예로 들면, 답이 없으면 NIE 을 출력하고, 답이 있으면 TAK 을 출력한 후 해당 답을 출력하는 문제들을 생각할 수 있다. 일반적으로 증거는 그냥 답 그 자체가 되는 경우가 많다. 딱히 그렇지 않을 이유가 없기 때문이다. 하지만, 그것이 정의상으로 강제되는 것은 아니고, 특정한 다른 프로그램 (예를 들어, Special Judge)을 통해서 주어진 증거를 토대로 효율적으로 답이 있음을 증명할 수 있어야 한다. 이러한 결정 문제의 예시로, 아래에 해밀턴 회로를 정의한다:

  • 해밀턴 회로: 그래프 $G$ 가 입력으로 주어졌을 때, $G$ 의 모든 정점을 지나는 단순 사이클이 있는지를 찾아야 한다. 만약 없으면 NIE 을 출력하고, 있으면 TAK 을 출력한 후 해밀턴 회로의 정점 번호 순서대로 $n$ 개의 정수를 출력한다.

결정 문제가 모든 알고리즘 문제를 포함하지는 않는다. 예를 들어, 경우의 수를 세거나, 최소화를 하는 문제들은 결정 문제로 해결할 수 없다. 하지만, 최대화를 하는 문제들에 대해서는, “문제의 답이 $k$ 이하인가?” 라는 식의 변형을 통해서 이를 결정 문제로 변형하는 테크닉이 존재한다. 예를 들어, 다음과 같은 문제를 생각해 보자:

  • 정점 덮개: 그래프 $G$ 가 정수 $k \geq 0$이 입력으로 주어졌을 때, $G$ 에서 최대 $k$ 개의 정점을 색칠하여, 모든 간선에 대해 양 끝점 중 하나가 색칠되어 있게 하는 것이 가능한 지 판별해야 한다. 만약 없으면 NIE 를 출력하고, 있으면 TAK을 출력한 후 $k$ 개 이하의 정수로 색칠한 정점들을 출력한다.

이제, 최소 정점 덮개를 구하는 것은, 답이 되는 인자 $k$ 에 대해서 이분 탐색을 하고, 처음으로 답이 되는 $k$ 를 찾아주는 것으로 가능한다. 즉, $\log N$ 번 결정 문제를 해결하면 최대화 문제로 환원할 수 있는 것이다. 이러한 테크닉이 항상 가능한 것은 아니고, 단지 가능한 해결 방법의 예시 중 하나를 소개한 것이다.

계산 복잡도 위계

먼저, 다음과 같은 4개의 계산 복잡도 그룹을 소개한다:

  • P: 결정 문제 $L$ 을 다항 시간복잡도에 결정할 수 있음.
  • NP: 결정 문제 $L$ 과 증거 $W$ 가 주어질 때 다항 시간에 검증할 수 있음.
  • PSPACE: 결정 문제 $L$ 을 다항 공간복잡도에 결정할 수 있음.
  • EXP: 결정 문제 $L$ 을 지수 시간복잡도에 결정할 수 있음.

NP는 다른 방법으로도 정의할 수 있다. 우리가 사용하는 C 프로그래밍 언어에 하나의 추가적인 함수, guess() 함수를 도입하자. 이 함수는 인자를 받지 않고 true / false 를 반환하며, $O(1)$ 시간 복잡도에 작동한다. 이러한 새로운 프로그래밍 언어를 비결정론적 C 언어 라고 부르자. (이는 일반적인 계산 이론에서 비결정론적 튜링 머신 이라고 부르는 것에 대응된다.)

이제 이 비결정론적 C 언어로 결정 문제 $L$를 해결하려 해 보자. 우리는 입력 $X$ 가 $L$ 을 만족하면 1, 아니면 0을 반환하는 프로그램을 만들려고 한다. 이 과정에서 우리는 guess() 함수를 사용할 수 있다. 이 때, guess() 함수는 어떠한 전지전능한 존재가 조종하고 있어서, 우리의 프로그램이 1을 반환할 수 있으면 1을 반환하게끔 최선을 다해서 결과값을 준다고 생각하자. 다른 말로 하면, 우리의 프로그램은 1을 반환시키는 적절한 guess() 수열이 있으면 1을 반환한다. 이러한 좋은 guess() 함수가 존재할 때, 우리는 이를 통해서 다항 시간에 결정 문제 $L$ 을 판정하고자 할 것이다.

예를 들어, 그래프의 정점 덮개 문제를 해결하는 비결정론적 C 언어 프로그램은 다음과 같이 구성되어 있을 것이다: 모든 $1 \le i \le V(G) $ 에 대해 $X_i$ 가 참이면 해당 정점을 색칠한다고 하자. X[i] = guess() 함수를 사용한 후, $\sum_{i=1}^{k} X_i \le K$ 이며, 모든 간선에 대해 한쪽 끝점이 $X_i = 1$ 을 만족하는 지 판정한다. 이 프로그램은 자명히 다항 시간 안에 작동하며, 만약 주어진 입력이 참이라면 전지전능한 guess() 가 1을 반환하게 좋은 색칠을 주겠지만, 그렇지 않다면 전지전능한 guess() 역시 수가 없어 0을 반환할 수 밖에 없을 것이다.

우리는 다음 정리를 증명한다.

Theorem 1. 어떠한 결정 문제 $L$ 가 비결정론적 C 언어 프로그램으로 다항 시간 안에 결정된다는 것은, $L \in NP$ 와 동치이다.

대강의 증명.

  • $\rightarrow$: 올바른 guess() 비트열이 증거가 되고, 비결정론적 C 언어 프로그램이 검증 프로그램이 된다.
  • $\leftarrow$: 증거 $W$ 는 입력에 대한 다항함수 내의 크기를 가지니, $W$의 모든 정보를 이진수로 판정하고 guess() 비트열로 $W$ 를 찾자. 찾은 이후, $W$가 주어질 때 0과 1을 반환하는 검증 프로그램을 그대로 구현하면 된다.

증명을 따라가다 보면 이해했겠지만, 사실 guess() 는 그냥 증거라는 개념을 다른 방법으로 서술한 것에 불과하다. 비결정론적 C 언어 프로그램의 문제 해결 방식은 검증 프로그램(Special Judge)와 거의 유사할 것이다.

이제 아래 정리를 증명한다.

Theorem 2. $P \subset NP \subset PSPACE \subset EXP$

**대강의 증명. **

  • $P \subset NP$: $L$ 을 푸는 올바른 프로그램이 증거 $W$가 된다.
  • $NP \subset PSPACE$: 검증 프로그램은 $P$ 이니 자명히 다항 공간복잡도 안에 수행된다. guess() 로 가능한 모든 수열을 나열한 후 검증 프로그램을 돌려 보면 된다.
  • $PSPACE \subset EXP$: 프로그램의 기작은 현재 상태의 메모리 구성이 어떻게 되어 있는지에만 따라 결정된다. 고로, 어떤 프로그램의 실행 과정에서 같은 메모리 구성이 두 번 이상 등장하였다면, 해당 프로그램은 무한 루프에 빠진다. 해당 프로그램이 사용하는 최대 메모리 양은 다항함수로 표현 가능하다. 이 비트 수를 $MAXMEM$ 이라 하자. PSPACE 프로그램은 $2^{MAXMEM} + 100$ step만큼 프로그램을 돌리면 결정이 되거나, 무한 루프에 빠진다. 후자는 가정에 모순이고, 고로 지수 시간 복잡도에 판정할 수 있다.

SAT 문제

어떠한 불리언 식이 $F = \bigwedge_{i} (\bigvee_{j} L_{i, j})$ 와 같은 형태로 구성되어 있을 시 ($L_{i, j}$ 를 리터럴(literal) 이라 부르며, 변수 내지는 변수의 negation이다.) 이러한 불리언 식은 CNF(conjunctive normal form) 형태라고 정의한다. 예를 들어, $(x_1 \lor x_2 \lor \lnot x_4) \land (x_3 \lor \lnot x_1) \land (\lnot x_4) \land (x_{5})$ 와 같은 것은 CNF이다. 직관적으로 보았을 때, CNF는 어떠한 조건이 성립하면 안 되는지 를 나열한 것이라고 할 수 있다. 이 때, 각 OR clause에 최대 $k$개의 리터럴만이 존재하면, 이를 $k$-CNF 라고 부른다. 예시로 든 불리언 식은 3-CNF이지만, 2-CNF는 아니다.

다음과 같은 두 가지 사실이 잘 알려져 있다. 증명은 생략한다.

  • Proposition 1. 임의의 불리언 식에 대해서 동치인 CNF가 존재한다.
  • Proposition 2. 모든 CNF는, 동치인 3-CNF로 다항 시간 안에 환원 가능하다.

이제 다음과 같은 결정 문제를 소개한다.

  • 3-SAT. 3-CNF $F$ 가 주어졌을 때, $F$ 를 참으로 만드는 변수 배정이 가능한가?

3-SAT은 자명히 NP이다. 모든 변수를 guess() 한 후 비트 연산을 하면 되기 때문이다. 한편, 3-SAT이 P인지 아닌지는 알려져 있지 않다.

이제, 환원이라는 개념을 도입한다.

  • 다항 시간 환원. 어떠한 결정 문제 $L$ 에 대해, 어떠한 결정 프로그램 $M$ 을 판정하는 C 함수를 한번 호출하고, 그 외 모든 것을 다항 시간 안에 해결해서 $L$ 을 판정할 수 있으면, $L$을 $M$ 으로 다항 시간 환원 할 수 있다고 하며 $L \leq_{p} M$ 으로 표기한다.

직관적으로, 거의 모든 NP 문제는 3-SAT으로 다항 시간에 환원 가능하다. guess() 는 결국 미지의 불리언 값이니 이를 변수로 두고, 모든 프로그램의 수행 과정은 결국 low-level에서는 비트 연산으로 표현 가능하니 각 시간의 모든 비트 상태를 전부 비트 변수로 저장하고, 이에 대한 관계식을 CNF의 형태로 표현한다. 이제 3-SAT을 부르면 guess() 결과가 나오니 이를 토대로 문제를 해결하는 것이다. 이 직관은 참이며, 1970년대 초반 아래와 같이 정리되었다.

  • Cook-Levin Theorem. 모든 NP 문제는 3-SAT으로 다항 시간 안에 환원 가능하다.
  • NP-Complete. 어떠한 문제 $L$ 에 대해, $L \in NP, 3SAT \leq_{p} L$ 이면 $L$ 은 NP-Complete이다. 고로 $L$ 을 풀면 3-SAT을 풀 수 있으며 반대도 성립한다.
  • Cook-Levin Theorem (alternative). 3-SAT은 NP-complete이다.
  • NP-Hard. $3SAT \leq_{p} L$ 이면 $L$ 은 NP-hard이다. 고로 $L$을 풀면 3-SAT을 풀 수 있으나, 반대는 성립하지 않을 수도 있다. NP-hard 문제가 NP에 속하지 않을 수 있다.

QBF 문제

SAT의 일반화된 형태는 QBF이다. QBF는, CNF 식 $F$ 가 주어졌을 때, $\exists x_1 \forall x_2 \exists x_3 \forall x_4 \cdots F$ 가 성립하는 지를 판별해야 한다. 이 때, $\exists x_1$ 은 $x_1 = true, x_1 = false$ 로 했을 때 중 하나는 참이 된다는 것이고, $\forall x_2$ 는 $x_2 = true, x_2 = false$ 모두 참이 된다는 것이다. 고로, 이 알고리즘을 재귀적으로 판정하는 것은 다음과 같이 가능하다:

  • 입력이 $Q_1 x_1 Q_2 x_2 \cdots F$ 와 같이 주어질 경우:
    • $E_0 = Q_2 x_2 \cdots F[false / x_1], E_1 = Q_2 x_2 \cdots, F[true / x_1]$ 이라 하자. $F[y/x]$ 는 모든 $x$ 를 $y$ 로 치환했다는 뜻이다.
    • $Q_1 = \exists$ 일 시 $E_0 \lor E_1$, $Q_1 = \forall$ 일 시 $E_0 \land E_1$ 을 반환한다.
  • 그 외 경우 $F$ 안에 변수가 없으니 그냥 계산하여 반환한다.

이러한 재귀적 알고리즘은 지수 시간 복잡도와 다항 시간 공간 복잡도에 판정 가능하다. 고로 QBF는 PSPACE이다. 여담으로, $\forall$ 연산자가 없이 $\exists$ 연산자만 존재한다면 QBF는 SAT 문제와 동일함을 관찰하자. 고로, SAT는 QBF의 특수한 경우라고 생각할 수 있다.

이제 다음 Theorem을 제시한다:

Theorem 4. 모든 PSPACE 문제 $L$ 에 대해, $L \leq_{p} QBF$.

Proof. $L$ 을 판정하는 프로그램이 최대 $s$ 비트의 메모리를 사용한다고 하자. 이 때 $s$ 는 입력 크기에 대한 다항 함수이다. $2^s$ 개의 정점을 가진 방향 그래프를 정의한다. 각 정점은 해당 비트에 대응되는 메모리 상태를 의미하며, 각 메모리 상태에는 유일한 다음 메모리 상태가 항상 존재한다. 모든 상태에서, 이러한 유일한 다음 메모리 상태로 가는 방향성 있는 간선을 잇는다.

이 때, $L$이 어떠한 입력을 판정한다는 것은 시작 상태 $v$ 에서 유일한 최종 상태 $w$ 로 가는 경로가 존재한다는 것과 동치이다. 경로가 존재하면 단순 경로가 존재하니 이 경로의 길이는 $2^s$ 이하라고 가정할 수 있다. $P(u, w, s)$ 를, 상태 그래프에서 $u \rightarrow w$ 로 가는 길이 $2^s$ 의 간선이 존재할 때 참이라고 정의하자. $s > 0$ 일 때, $P(u, w, s) = \exists v P(u, v, s-1) \land P(v, w, s-1)$ 이다. 다르게 표현하면, $\exists v \forall s \forall t ((s = u) \land (t = v)) \lor ((s = v) \land (t = w)) \rightarrow P(s, t, s - 1)$ 과 동치이다. QBF는 불리언 식만을 수용하지만, 결국 정점 번호는 $s$ 비트의 정수이니 불리언 변수로 분리할 수 있음을 기억하자. 고로 크기 $s$ 의 QBF 식을 만들었다.

PSPACE가 있으면 NPSPACE도 있다고 생각할 수 있고, 실제로 그렇다. 위에서 정의한 것과 같이 다항 공간 복잡도 안에 비결정론적 C 프로그램이 문제를 해결할 수 있다면, 어떠한 결정 문제는 NPSPACE에 속한다. 하지만 NPSPACE가 무의미한 것은, $PSPACE = NPSPACE$ 이기 때문이다.

Savitch’s Theorem. 모든 다항식 $p$에 대해, $NSPACE(p) \subset PSPACE(p^2)$.

증명은 Theorem 3과 비슷하며 생략한다.

2-CNF Formulas

위에서 3-CNF을 정의하고, 3-CNF에 대한 Satisfiability, QBF Problem에 대해서 소개하였다. Satisfiability에서조차 3-CNF를 효율적으로 해결하는 방법은 알려져 있지 않고, $P=NP$ 가 아닌 이상 아마 없을 것으로 추정되지만, 각 clause에 최대 2개의 항이 들어 있을 수 있는 2-CNF의 경우에는, 놀랍게도, SAT 문제와 QBF 문제를 모두 효율적으로 해결할 수 있는 방법이 알려져 있다.

2-CNF는 SAT와 QBF 모두 선형 시간, 즉 가능한 가장 효율적인 시간 복잡도에 판정 가능하며, 이 방법은 1979년 Aspvall, Plass, Tarjan에 의해서 발표되었다. 2-CNF에 대한 SAT 문제를 해결하는 풀이는 흔히 2-SAT이라고 불리며 문제 해결용 알고리즘 커리큘럼에 대다수 들어갈 정도로 잘 알려져 있지만, 2-QBF에 대해서는 아는 사람들이 거의 없다. 최근 NEERC 2018에서 2-QBF의 Evaluation을 요구하는 문제가 출제되었고, 이후 이러한 문제들이 대중화 될 가능성도 있어 보여서 이에 대해서 설명한다. 이 글을 읽는 독자들이 강연결 컴포넌트 (Strongly connected component) 에 대한 지식이 있음을 가정하고 풀이를 설명하며, 2-SAT 문제를 해결하는 방법을 안다면 글을 이해하기 훨씬 쉬울 것이다.

2-CNF를 해결하기 위해서는 Implication Graph라는 것을 사용한다. 일반성을 잃지 않고, 모든 clause가 2개의 항을 가지고 있다고 가정하자 (1개의 항을 가지고 있다면, $x_i$ 를 $x_i \lor x_i$ 로 바꿔주면 2개로 변환 가능하다). 아이디어는, $(u \lor v) \equiv (\lnot u \rightarrow v)$ 라는 관계가 성립한다는 것이다. 고로, 각 변수를 정점, 그리고 이러한 함의(implication) 관계를 방향성 간선으로 해석하여서, 문제를 해결한다.

Implication Graph의 정점은 등장하는 각 변수, 그리고 각 변수의 negation들로 구성되어 있다. 고로, $x_1, \cdots, x_n$ 이 주어지면 $(x_1, \cdots, x_n, \lnot x_1, \cdots, \lnot x_n)$ 과 같은 $2n$ 개의 정점이 존재하는 것이다. 간선은 각 clause마다 2개씩 만들어지는데, $(u \lor v)$ 와 같은 clause가 등장하면, $(\lnot u, v), (\lnot v, u)$ 의 2개의 방향성 간선을 잇는다.

이 때, 다음 정리를 사용하면, 2-QBF의 해결 가능 여부가 간단한 그래프 탐색 문제들로 환원됨을 알 수 있다:

Theorem 6. 2-CNF $F$ 에 대해서, $Q_1 x_1 Q_2 x_2 \cdots F$ 가 참임은, $F$ 에 대한 Implication graph $G$ 가 아래 조건을 모두 만족함과 동치이다:

  • $Q_i = \exists$ 일 때, $x_i \rightarrow \lnot x_i$ 로 가는 경로와 $\lnot x_i \rightarrow x_i$로 가는 경로 중 하나는 존재하지 않는다. (고로, $x_i, \lnot x_i$ 는 다른 SCC에 있다.)
  • $Q_i = \exists, Q_j = \forall, i < j$ 일 때, $x_i \rightarrow x_j$ 로 가는 경로와 $x_j \rightarrow x_i$로 가는 경로 중 하나는 존재하지 않는다. (고로, $x_i, x_j$ 는 다른 SCC에 있다.)
  • $Q_i = \forall$ 인 모든 $i = {k_1, k_2, \cdots, k_m}$ 에 대해, ${x_{k_1}, \lnot x_{k_1}, \cdots, x_{k_m}, \lnot x_{k_m}}$ 에 있는 임의의 서로 다른 두 정점을 잇는 경로는 존재하지 않는다. (고로, 위에서 등장하는 변수들은 모두 다른 SCC에 있으며, 이들이 등장하는 SCC는 반사슬을 이룬다.)

증명.

먼저 Implication graph에서는 어떠한 한 변수가 참이 될 때, 이 변수가 도달할 수 있는 모든 변수는 모두 참이 되어야 한다는 성질이 있음을 관찰하자. 모든 간선은 특정한 함의를 대표하고 있기 때문에, 어떠한 변수가 참이 되면, 이 변수가 함의하는 다른 변수들도 참이 되고, 그들이 함의하는 다른 변수들도 모두 참이 되는 것이 계속된다. 이 증명에서는 이러한 성질을 계속 활용할 것이다.

$\rightarrow$ :

  • 만약 $x_i \rightarrow \lnot x_i, \lnot x_i \rightarrow x_i$ 경로가 모두 존재한다면, $x_i$ 가 참일 경우 $\lnot x_i$ 역시 참이 되어야 해서 모순이고, $\lnot x_i$ 가 참일 경우 $x_i$ 역시 참이 되어야 해서 모순이다.
  • 만약 $x_i \rightarrow x_j, x_j \rightarrow x_i$ 경로가 모두 존재한다면, $x_i$ 를 참으로 결정한다면 $x_j$ 를 거짓으로 결정할 수 없게 된다. $x_i$ 를 거짓으로 결정한다면 $x_j$ 를 참으로 결정할 수 없게 된다.
  • 만약 임의의 서로 다른 두 정점 $u \rightarrow v$ 를 잇는 경로가 존재한다고 하자. $u, v$가 같은 clause일 경우 첫 번째 조건에 의해 자명히 모순이다. 다른 clause일 경우, $u$ 가 참이고 $v$ 는 거짓이면 모순이 된다. 고로 $\forall$ 문에서 고를 수 없는 조건이 생겨서 모순이다.

$\leftarrow$:

$G$ 의 각 강연결 컴포넌트를 다음과 같이 분류하자.

  • $A$: $\forall$ 수량자가 있는 정점들에 해당하는 컴포넌트.
  • $T$: $\forall$ 수량자가 있는 컴포넌트 중 하나에서 도달 가능하며, $A$가 아닌 컴포넌트.
  • $F$: $\forall$ 수량자가 있는 컴포넌트 중 하나를 도달 가능하며, $A$가 아닌 컴포넌트.
  • $B$: 셋 다 아님.

이 때 모든 컴포넌트는 네 종류 중 하나로 항상 분류할 수 있다. 이는 가정에 의해 $A$가 반사슬이고, $T$ 와 $F$에 교집합이 존재한다면 모순이 (강연결 컴포넌트가 바뀌거나, 반사슬 가정이 깨지는) 생기기 때문이다. 이제 각 컴포넌트에 있는 $\exists x_i$변수에 다음과 같이 값을 지정한다:

  • $A$에는, 해당 SCC에 있는 유일한 $\forall$ 변수와 같은 값. 즉, 해당 컴포넌트에 ${x_3, \lnot x_4, x_6}$ 이 있고 $\forall x_3 \exists x_4 \exists x_6$ 이면 $x_4 = \lnot x_3, x_6 = x_3$ 이다. 이 때 $\forall$ 변수는 내가 배정하는 변수보다 먼저 등장하기 때문에 (bound variable) 잘 정의된다. 이렇게 되는 이유는 두번째 조건에서 알 수 있다.
  • $T$에는 true
  • $F$에는 false.
  • $B$에는, SCC의 topological ordering $t$ 에서 $t(\lnot x) < t(x)$ 이면 true, 아니면 false.

먼저, 이 배정이 가능함을 보인다. 즉, exists의 경우 $x, \lnot x$에 같은 값을 매기는 일이 없어서 올바른 배정으로 바로 변환할 수 있음을 보인다.

  • $v \in T \iff \lnot v \in F$ 가 성립한다. 어떠한 forall 정점에서 $v$로 가는 경로를 생각했을 때, 이들의 대우명제로 이루어진 경로가 존재하기 때문이다. 고로 $T, F$ 에 있는 원소들은 모순이 없다.
  • $v \in A$ 이면, 해당 $v$에 값을 제공한 forall 항은 $\lnot v$에도 대우명제 경로를 통해 똑같은 항을 제공하여 모순을 이루지 않는다.
  • $v \in B$ 이면, 위 두 명제에 에 의해 $\lnot x \in B$ 이다. 고로 모순을 이루지 않는다.

이제 이 배정이 올바름을 보인다. 이는, 어떠한 forall 배정에 대해서도 모든 간선에 대해서 참 -> 거짓 방향이 없음을 통해 보인다. 모든 컴포넌트에 같은 값이 배정되었기 때문에 그러한 간선은 서로 다른 강연결 컴포넌트를 잇는다. 이 때 몇 가지 케이스를 분석한다.

  1. $T \rightarrow {A, B, T, F}, {A, B, T, F} \rightarrow F$. 고려할 필요가 없거나 ($T \rightarrow T, F \rightarrow F$) $T, F$ 의 정의에 모순이다.
  2. $F \rightarrow {A, B, T, F}, {A, B, T, F} \rightarrow T$, 고려할 필요 없다.
  3. $B \rightarrow A, A \rightarrow B$. $B$ 의 정의에 모순이다.
  4. $A \rightarrow A$. 반사슬 가정에 모순이다.
  5. $B \rightarrow B$. 이 간선을 $x \rightarrow y$ 라 하자. 배정에 의해 $t(\lnot x) < t(x) < t(y) < t(\lnot y)$ 이다. 한편 대우명제 간선이 $\lnot y \rightarrow x 를 잇는다. 위상정렬 순서라는 가정에 모순이다.
  • \4. B->A, A->B. B의 정의에 모순이다.
  • \5. F->*, *->T. 고려할 필요 없다.

이로써 모든 케이스에 대해 증명하였다.

Theorem을 증명했으니, 이제 $F$ 가 주어졌을 때 다음과 같은 알고리즘을 설계할 수 있다:

  • $F$ 에 대한 Implication graph $G$ 를 만들고 SCC를 선형 시간에 계산한다.
  • 첫 번째 조건은 자명히 선형 시간 안에 계산할 수 있으며, 두 번째 조건은 각 SCC에 대한 배열을 만들고 $i$를 증가시키면서 체크하는 식으로 역시 선형 시간 안에 계산할 수 있다.
  • 마지막 조건은, SCC를 통해 만든 그래프가 DAG이기 때문에 동적 계획법으로 처리할 수 있다. 먼저 각 변수가 모두 다른 SCC에 있는 지를 배열을 통해서 간단히 체크한다. 이제 위에서 $\forall$ 에 의해서 체크된 SCC를 나쁜 컴포넌트 라고 정의한다 이후, $DP_i$ 를, 해당 SCC에서 도달 가능한 컴포넌트 중 나쁜 컴포넌트가 존재하는가? 라고 정의한다. $DP_i$ 는 선형 시간에 채울 수 있고, 모든 나쁜 컴포넌트 $i$에 대해서, 해당 컴포넌트에서 나가는 간선 $i \rightarrow j$ 가 있는 컴포넌트 중 $DP_j$ 가 참인 것이 있는 지를 확인하면 된다. 모두 선형 시간에 계산된다.

이 알고리즘의 구현체는 koosaga github에 공개되어 있다.