1.7 Horn Formulas
Horn formula란 CNF formula의 특별한 형태를 의미. 이 Sec.에서는 Horn formula가 satisfiable인지 아닌지 결정하는 빠른 방법을 소개한다.1
—
Definition 1.7.1
Horn formula란 모든 disjunction이 많아야 하나의 positive literal을 포함하는 CNF formula를 말한다.
—
명백히 두 Horn formula의 conjunction은 Horn formula.
—
Example 1.7.2
$A \wedge (\neg A \vee \neg B \vee C) \wedge (\neg B \vee D)\wedge (\neg C \vee \neg D)$는 Horn formula.
$A \vee B$는 Horn formula가 아니다.
—
Basic Horn formula는 $\wedge$가 쓰이지 않은 Horn formula를 말한다. 예를 들어, $(\neg A \vee \neg B \vee C)$, $A$, $(\neg B \vee \neg D)$는 basic Horn formula이다. 모든 Horm formula는 basic Horn formula들의 conjunction.
Basic Horn formula에는 세 가지 유형이 존재한다.:
- Positive literal이 포함되지 않은 것. ex) $(\neg A \vee \neg B \vee C)$
- Negative literal이 포함되지 않은 것. ex) $A$
- Positive literal과 negative literal을 모두 포함하는 것. ex) $(\neg B \vee \neg D)$
만약 basic Horn formula가 positve와 negative literal을 모두 포함한다면, positive literal들만 갖는 implication으로 쓸 수 있다. 예를 들어,
\[(\neg A \vee \neg B \vee C) \equiv (A \wedge B) \rightarrow C\]
만약 basic Horn formula가 positve literal을 포함하지 않는다면, contradiction에 관한 implication으로 쓸 수 있다. 예를 들어,
\[(\neg B \vee \neg D) \equiv (B \wedge D) \rightarrow \perp\]
만약 basic Horn formula가 negative literal을 포함하지 않는다면, 이는 atomic formula이며 원한다면 implication으로 쓸 수 있다. 예를 들어,
\[A \equiv T \rightarrow A\]
여기서 $T$는 tautology를 뜻한다.
이로써 모든 basic Horn formula는 implication으로 쓸 수 있고, 모든 Horn formula는 implication의 conjunction으로 쓸 수 있다.
—
Example 1.7.3
Ex. 1.7.2의 Horn formula는 다음과 같이 쓸 수 있다.
\[(T \rightarrow A) \wedge ((A \wedge B ) \rightarrow C) \wedge (B \rightarrow D) \wedge ((C \wedge D) \rightarrow \perp) \]
—
Horn formula $H$가 주어졌을 때, $H$가 satisfiable인지 아닌지를 결정하고 싶다. 이 decision problem을 Horn Satisfiability Problem(HORNSAT)라고 한다. 지금까지 봐 온 decision problem들과는 달리, HORNSAT에는 풀이를 위한 효과적인 알고리즘이 존재한다. Implication들의 conjunction들로 이루어진 어떤 Horn formula가 있다고 하자.
—
Horn Algorithm
Implication들의 conjunction으로 쓰여진 Horn formula $H$가 주어졌을 때, $H$에 등장하는 atomic formula들을 나열한다.
-
Step 1 : $(T \rightarrow A)$ 형태의 subformula 내에 있는 각 atomic formula $A$를 표시한다.
-
Step 2 : 만약 $ (A_{1} \wedge A_{2} \wedge \dots \wedge A_{m}) \rightarrow C$ 형태의 subformula가 존재하고, 각 $A_{i}$가 표시되어 있으나 $C$가 표시되어 있지 않다면, $C$를 표시한다. 이러한 형태의 subformula가 더이상 존재하지 않을 때까지 이 단계를 반복하고 다음으로 넘어간다.
-
Step 3 : $(A_{1} \wedge A_{2} \wedge \dots \wedge A_{m}) \rightarrow \perp$ 형태의 subformula를 생각한다.
만약 각 $A_{i}$가 표시된 이런 형태의 subformula가 존재한다면, 다음 결론을 내린다:
\[``H \textrm{ is not satisfiable.}”\]
그렇지 않다면,
\[``H \textrm{ is satisfiable.}”\]
—
Example 1.7.4
$H$를 다음 formula라고 하자.
\[(T \rightarrow A) \wedge (C \rightarrow D) \wedge ((A \wedge B) \rightarrow C) \wedge ((C \wedge D) \rightarrow \perp) \wedge (T \rightarrow B) \]
$H$의 atomic subformula는 $A$, $B$, $C$, $D$이다.
-
Step 1 : $H$가 subformula $(T \rightarrow A)$와 $(T \rightarrow B)$를 가지므로 $A$와 $B$를 표시한다.
-
Step 2 : $H$가 subformula $(A \wedge B) \rightarrow C$를 가지고 $C$가 표시되어 있지 않으므로 $C$를 표시한다. 이제 $C$가 표시되었으므로 subformula $(C \wedge D)$에서 $D$를 표시할 수 있다.
-
Step 3 : $H$가 subformula $(C \wedge D) \rightarrow \perp$를 가지므로 알고리즘은 다음 결론을 내린다:
\[``H \textrm{ is not satisfiable.}”\]
$\square$
—
이제 임의의 주어진 Horn formula에 대해 Horn Algorithm이 빠르게 작동한다는 것을 보이려고 한다. 먼저 필요한 것은, 정말로 “제대로” 작동하는가?
—
Proposition 1.7.5
Horn Algorithm이 $``H \textrm{ is satisfiable.}”$이라는 결론을 낸다. iff $H$는 satisfiable이다.
—
Proof.
$\mathcal{S}=\{C_{1}, C_{2}, \dots C_{n}\}$을 $H$에 나타나는 atomic formula들의 set이라고 하자. 알고리즘이 결론을 내린 후에는 이들 중 몇몇은 표시가 되어 있을 것이다.
$[ \Leftarrow ]$ $H$가 satisfiable이라고 하자. 그러면 $\mathcal{S}$의 assignment $\mathcal{A}$가 존재해, $\mathcal{A} \models H$이다.(Def. 1.2.5) $H$의 각 Horn subformula $B$에 대해 $\mathcal{A} (B)=1$이 된다.
만약 $B$가 $(T \rightarrow C_{i})$ 형태라면, $\mathcal{A} (C_{i})=1$이다.
만약 $B$가 $(C_{1} \wedge C_{2} \wedge \dots \wedge C_{m}) \rightarrow D$ 형태이고 각 $\mathcal{A} (C_{i})=1$이라면, $\mathcal{A} (D)=1$이다. 이는 $\mathcal{A} (C_{i})=1$인 각 $C_{i}$가 표시되어 있다는 의미이다.
이제 귀류법을 사용해 알고리즘이 $``H \textrm{ is not satisfiable.}”$이라는 결론을 내렸다고 하자. 이는 오직 $B$의 subformula 중 $(A_{1} \wedge A_{2} \wedge \dots \wedge A_{m}) \rightarrow \perp$ 형태가 존재하고, 각 $A_{i}$가 표시되어 있을 때에만 발생한다. 각 $A_{i}$가 표시되어 있으므로, $\mathcal{A} (A_{i}) = 1$이다. $\rightarrow$의 semantics(http://younghwanjoo1608.github.io/logics/prl1.1/#definition-118)에 따르면, $\mathcal{A} (B)=0$을 얻게 되고 이는 모순이다.
따라서, 만약 $H$가 satisfiable이면, 알고리즘은 $``H \textrm{ is satisfiable.}”$이라는 결론을 낸다.
$[ \Rightarrow ]$ Horn Algorithm이 $``H \textrm{ is satisfiable.}”$이라는 결론을 냈다고 가정하자. $\mathcal{S}$의 assignment $\mathcal{A}_{0}$를 $[ \mathcal{A}_{0} (C_{i}) = 1 \textrm{ iff } C_{i} \textrm{ is marked.} ]$로 정의하자. $\mathcal{A}_{0} \models H$를 보이고 싶다. $\mathcal{A}$가 $H$의 모든 Horn subformula들을 model함을 보이면 충분하다.
$B$를 $H$의 basic Horn formula라고 하자. 만약 $B$가 $(T \rightarrow A)$ 형태를 가지면, Step 1로부터 $A$가 표시되고 $\mathcal{A}_{0} (B)=1$이다.
그게 아니라면 $B$는 $ (A_{1} \wedge A_{2} \wedge \dots \wedge A_{m}) \rightarrow G$형태를 갖는다. 여기서 $G$는 atomic formula 또는 $\perp$이다. 만약 어떤 $i$에 대해 $\mathcal{A}_{0} (A_{i}) = 0$이면, $\mathcal{A}_{0} (B)=1$이 된다.(Table 1.1.4) $\mathcal{A}_{0}$가 각 $ A_{i}$를 model한다고 가정하자. 그러면 각 $ A_{i}$는 표시되어 있다. 알고리즘이 $``H \textrm{ is satisfiable.}”$이라는 결론을 냈으므로, $G$는 $\perp$일 수 없다. 즉 $G$는 atomic formula. 각 $ A_{i}$는 표시되어 있고, Step 2에 따라 $G$도 표시되므로 $\mathcal{A}_{0} (G)=1$. 이로부터 어느 경우든 $\mathcal{A}_{0} (B)=1$를 얻는다.
$H$의 모든 basic Horm formula들이 $\mathcal{A}_{0}$로 model되므로, $\mathcal{A}_{0} \models H$이고, $H$는 satisfiable. $\square$
—
Horn Algorithm이 정말로 제대로 작동함을 알 수 있다. 임의의 Horn formula $H$가 주어지면, 알고리즘은 $H$가 satisfiable인지 아닌지 정확히 판단한다.
그럼, 결론에 다다르기까지 Horn Algorithm은 얼마나 많은 step을 거쳐야 하는가?
답은 $H$의 길이에 달려 있다. $H$가 $n$개 symbol(기호)로 이루어진 string(문자열)이라면 ($n$은 큰 자연수) Horn Algorithm은 $n^{2}$보다 적은 step에서 결론을 내린다.
이를 입증하기 위해 Horn Algorithm의 step을 세어 보자. 2
먼저, $H$를 왼쪽부터 읽어나가며 모든 atomic subformula를 나열하자. $H$가 $n$개 symbol을 가지므로,최대 $n$개의 atomic formula들의 목록이 존재할 것이다. $(1 \textrm{ step})$
이제 Step 1에서 $H$를 다시 읽어내리는데, 이번에는 tautology $T$가 존재하는지를 확인하고, 이에 따라 적절하게 atomic formula를 표시해나간다. $(1 \textrm{ step})$
Step 2에서는 각 $A_{i}$들이 표시된 $ (A_{1} \wedge A_{2} \wedge \dots \wedge A_{m}) \rightarrow C$ 꼴의 subformula를 찾는다. 만일 발견한 formula에 $C$가 표시되어 있지 않다면, 표시한다. 새로운 atomic formula가 표시되었으니 각 $A_{i}$들이 표시된 $ (A_{1} \wedge A_{2} \wedge \dots \wedge A_{m}) \rightarrow C$ 꼴의 subformula가 새로 발생했을 수 있다. 다시 $H$를 읽어내린다. 최대 $n$개의 atomic formula를 표시할 수 있으므로, $n$회보다 많이 Step 2를 반복할 필요는 없다. $(n \textrm{ step})$
마지막으로 Step 3에서는 $\perp$를 찾으며 $H$를 한 번 읽어내리고 결론에 도달한다. $(1 \textrm{ step})$
도합, $H$를 최대 $1+1+n+1=n+3$회 읽어내려야 결론에 도달한다. $n>2$일 때 $n^{2}>n+3$이므로, 이는 우리의 주장을 뒷받침한다. 그래서, 이 알고리즘은 빠르다고 할 수 있을까?
—
Definition 1.7.6
알고리즘이 polynomial-time(다항 시간)이라는 것은 다항식 $p(x)$가 존재하여, 주어진 size $n$의 input에 대해 알고리즘이 $p(n)$보다 적은 step 안에 정지한다(halt)는 것을 말한다.
어떤 polynomial-time algorithm에 의해 해결(resolve)될 수 있는 모든 decision problem들의 class를 $\mathbf{P}$로 나타낸다.
—
만약 알고리즘이 polynomial-time이 아니면, 그건 빠르지(quick) 않은 것. 따라서 Horn Algorithm은 polynomial-time이고 HORNSAT는 $\mathbf{P}$에 속한다. 이와 대조되는 다른 decision problem들을 살펴 보자.
- Validity Problem : Formula $F$가 주어졌을 때, $F$는 valid한가?
- Satisfiability Problem : Formula $F$가 주어졌을 때, $F$는 satisfiable한가?
- Consequence Problem : Formula $F$와 $G$가 주어졌을 때, $G$는 $F$의 consequence인가?
- Equivalence Problem : Formula $F$와 $G$가 주어졌을 때, $F$와 $G$는 equivalent한가?
어떤 면에서 봤을 때, 이 문제들은 모두 같다. 이 중 하나에서 작동되는 알고리즘은 다른 것들에도 작동한다.
- 만일 Validity problem에 대한 알고리즘을 가지고 있다면, 이를 Satisfiability problem을 해결할 때 사용할 수 있다. $[F \textrm{ is satisfiable iff } \neg F \textrm{ is not valid}]$이기 때문.
- Satisfiablity problem의 알고리즘으로 Consequence problem이 해결된다. $[G \textrm{ is a consequence of }F \textrm{ iff } \neg (F \rightarrow G) \textrm{ is not satisfiable}]$이기 때문.
- Consequence problem의 알고리즘을 두 번 사용해 Equivalence problem이 해결된다.
- Equivalence problem을 해결하는 알고리즘이 있으면, $F$가 기지의 tautology $T$와 동치인지를 판단할 수 있으므로, Validity problem이 해결된다.
- 특히 이 네 가지 중 하나가 $\mathbf{P}$에 속하면, 다른 것들도 그러하다.
진리표는 이들 문제를 각각 해결할 수 있는 알고리즘을 제공한다. Satisfiability problem을 예로 들어, 먼저 $F$의 진리표를 작성하고 진릿값이 한 번이라도 $1$이 되는지를 확인한다. 이 알고리즘은 분명 잘 작동한다. 그럼 얼마나 많은 step이 필요할까?
$F$가 $n$개의 atomic formula를 지니면, 진리표는 $2^{n}$개의 행을 가진다. 이들 행에 대한 진릿값을 계산할 때마다 $F$를 읽어야 하므로, input을 최소 $2^{n}$회 읽어야 한다. 이는 exponential이지 polynomial이 아니다.
임의의 주어진 다항식 $p(x)$에 대해, 충분히 큰 $n$에서 $2^{n}$은 $p(n)$보다 크므로, 이 알고리즘은 polynomial-time이 아니다.
Satisfiability problem(과 나머지 세 problem들)이 $\mathbf{P}$에 속하는지는 알려져 있지 않다. 즉 satisfiability를 위한 polynomial-time 알고리즘이 존재하는지를 모른다. 3 그러한 알고리즘을 만약 발견한다면, $\mathbf{P=NP}$ 문제가 해결되는 것!4
이 Sec.에서는 Satisfiability problem을 해결하는 진리표의 대체 수단으로 알고리즘을 이야기했다. Formal proof 역시 진리표를 대신할 수 있으나, 이것으로는 항상 decision problem을 해결할 수는 없다. 주어진 formula $F$에 대해, $F$가 unsatisfiable임은 formal proof로 보일 수 있으나$(\varnothing \vdash \neg F)$, $F$가 satisfiable인지는 보일 수 없다. 유사하게, formal proof는 formula가 valid인지, 다른 무언가의 consequence인지를 밝힐 수 있으나, 그렇지 않다는 것은 보일 수 없다.
만일 $\{ F \} \vdash G$에 대한 formal proof를 발견했다면, $``G \textrm{ is a consequence of }F”$라고 바로 결론내릴 수 있다. 그런데 만약 $G$가 $F$의 consequence가 아니라면…? 이런 decision proble을 위한 알고리즘은 다음 Sec.에.5