Tseytin変換

命題論理式を充足可能性が等価な連言標準形に変換する方法であるTseytin変換（Tseytin Transformation）について紹介します．

命題論理式の充足可能性問題

命題記号，真偽値を表す記号である真 $\top$ と偽 $\bot$ ，そして，論理記号 $\land, \lor, \lnot, \to, \leftrightarrow$ を組合せることによって作られる命題を 命題論理式（propositional formula）と呼びます．BNF記法を用いると，命題論理式は次の通りです．ただし， $P$ は命題記号です．

　 $A ::= \top \mid \bot \mid P \mid \lnot A \mid A \land A \mid A \lor A \mid A \to A \mid A \leftrightarrow A$

BNF記法で作られる命題論理式は木の構造を表します．例えば命題論理式 $\phi := ((p \lor q) \land r) \to \lnot s$ の木構造は次の通りになります．
　　　　 f:id:tatanaideyo:20181229212822p:plain:w300

命題論理式の各命題記号の真偽値を割り当て決めると，その命題論理式の真偽値が定まります．与えられた命題論理式を真とする真偽値割り当てが存在するかどうかを判定する問題は 充足可能性問題（satisfiability problem; SAT）と呼ばれています．上の命題論理式 $\phi$ は充足可能です．なぜならば，命題記号の真偽値割り当てを $(p, q, r, s) = (\top, \top, \top, \bot)$ とすると $\phi$ が真となるからです．

命題論理式を標準形と呼ばれる形に変換するとSATの問題が議論しやすくなります．よく使われる形に 連言標準形（Conjunctive normal form; CNF）があります．CNF は1つ以上のリテラルの論理和を1つ以上含む論理積の形式です．
　・リテラル（literal）：命題記号またはその否定（eg. $p$ または $\lnot p$ ）
　・節（clause）：1つ以上のリテラルを論理和で結んだ命題論理式（eg. $p \lor q \lor \lnot r$ ）
　・CNF：1つ以上の節を論理積で結んだ命題論理式（eg. $(p \lor q) \land (\lnot r) \land (\lnot p \lor r)$ ）

命題論理式をCNFに変換する方法として，次の法則を使用することが考えられます．
　1.　 $\lnot \lnot p \Longleftrightarrow p$
　2.　 $p \to q \Longleftrightarrow \lnot p \lor q$
　3.　 $p \leftrightarrow q \Longleftrightarrow (p \to q) \land (q \to p)$
　4.　 $\lnot(p \lor q) \Longleftrightarrow \lnot p \land \lnot q$
　5.　 $\lnot(p \land q) \Longleftrightarrow \lnot p \lor \lnot q$
　6.　 $(p \lor q) \land r \Longleftrightarrow (p \land r) \lor (q \land r)$
　7.　 $(p \land q) \lor r \Longleftrightarrow (p \lor r) \land (q \lor r)$

1番目は「二重否定の除去」，2番目は「含意の除去」，4・5番目はド・モルガンの法則，6・7番目は分配法則と呼ばれているものです．その他にも交換法則や冪等法則なども暗黙的に使用しますがここでは紹介しません．
命題論理式 $\phi := ((p \lor q) \land r) \to \lnot s$ を上の法則が適用できなくなるまで行った結果の CNF は $(\lnot p \lor \lnot r) \land (\lnot q \lor \lnot r) \land (\lnot s)$ となります．一見するとこの方法でも良さそうに思えますが次のような命題論理式 $(p_1 \land p_2) \lor (p_3 \land p_4) \lor \cdots \lor (p_{n-1} \land p_{n})$ を変換すると節の数が $n$ に関して指数関数的に増加します．そこで，サイズが変換前の線形サイズに抑えられるような変換を見つけたい気持ちになります．そこで登場するのが Tseytin変換です．
上の変換では任意の真偽値割り当てに対して変換前と変換後の命題論理式の真偽値が等しくなるような変換方法でした．その部分は妥協して，SATにおいて充足可能性が保たれるような CNF への変換を考えます．

命題論理式 $\phi := ((p \lor q) \land r) \to \lnot s$ を例に説明します． $\phi$ の木構造の葉の方から新たな命題記号に置き換えながら変換します．
　1. $\, (p \lor q)$ を $x_1$ に置き換える
　2. $\, (x_1 \land r)$ を $x_2$ に置き換える
　3. $\, (\lnot s)$ を $x_3$ に置き換える
　4. $\, (x_2 \to x_3)$ を $x_4$ に置き換える
　　 f:id:tatanaideyo:20181229231001p:plain:w300

置き換え前の部分命題論理式と置き換え後の命題記号は同値ではないといけません．なので，
　1'. $\, x_1 \leftrightarrow (p \lor q)$
　2'. $\, x_2 \leftrightarrow (x_1 \land r)$
　3', $\, x_3 \leftrightarrow (\lnot s)$
　4', $\, x_4 \leftrightarrow (x_2 \to x_3)$
がすべて成立つ必要があるので， $\phi$ は充足可能性を保ったまま次の命題論理式 $\phi'$ に変換されます．
　 $\phi' := (x_4) \land (x_4 \leftrightarrow x_2 \to x_3) \land (x_3 \leftrightarrow \lnot s) \land (x_2 \leftrightarrow x_1 \land r) \land (x_1 \leftrightarrow p \lor q)$

一般的に上の置き換えを行うと，各括弧の中身は1つの命題記号か，2つの命題記号 $x, y$ で $x \leftrightarrow \lnot y$ か，3つの命題記号 $x, y, z$ と論理記号 $\circ \in \{\lor, \land, \to, \leftrightarrow\}$ で $x \leftrightarrow (y \circ z)$ となっているかのいずれかです．各括弧の中身を書き直すと次のようになります．

　・ $\, x \leftrightarrow \lnot y \Longleftrightarrow (x \lor y) \land (\lnot x \lor \lnot y)$
　・ $\, x \leftrightarrow (y \lor z) \Longleftrightarrow (x \lor \lnot y) \land (x \lor \lnot z) \land (\lnot x \lor y \lor z)$
　・ $\, x \leftrightarrow (y \land z) \Longleftrightarrow (\lnot x \lor y) \land (\lnot x \lor z) \land (x \lor \lnot y \lor \lnot z)$
　・ $\, x \leftrightarrow (y \to z) \Longleftrightarrow (x \lor y) \land (x \lor \lnot z) \land (\lnot x \lor \lnot y \lor z)$
　・ $\, x \leftrightarrow (y \leftrightarrow z) \Longleftrightarrow (x \leftrightarrow y \to z) \land (x \leftrightarrow z \to y)$ （上の同値変形を使用）

よって， $\phi'$ を上の変換にしたがって変更すると，括弧内はすべて CNF となるのでTseytin変換後の命題論理式も CNF となります．しかも，各節に含まれるリテラル数が高々3の 3-CNF となります．命題論理式 $\phi$ をTseytin変換した後の CNF を $T(\phi)$ と表すと次のようになります．
　 $T(\phi) := (x_4) \land (x_4 \lor x_2) \land (x_4 \lor \lnot x_3) \land (\lnot x_4 \lor \lnot x_2 \lor x_3) \land$
　　　　　　 $(x_3 \lor \lnot s) \land (\lnot x_3 \lor s) \land (\lnot x_2 \lor x_1) \land (\lnot x_2 \lor r) \land$
　　　　　　 $(x_2 \lor \lnot x_1 \lor \lnot r) \land (x_1 \lor \lnot p) \land (x_1 \lor \lnot q) \land (\lnot x_1 \lor p \lor q)$

変換前の命題論理式に含まれる論理記号の数を $m$ とすると，新たに加えられた命題記号は $m$ 個で，節の数も高々 $6m$ 個となります．よって，Tseytin変換後の CNF の長さは高々 $18m$ となり，変換前の線形サイズで抑えることができました．また，このアルゴリズムは木構造の根からボトムアップでできるので $O(m)$ 時間でできます．

まとめ

「Tseytin」ってどう発音するんだろう．