充足可能性問題（SAT）で問題を解かせるには、変数を連言標準形（CNF）にする必要があります。ところが、実際に条件を組み立てていこうとすると、CNFに沿わない形となってしまうことも多々あります。ここでは、そのような論理式をCNFに変形するTseitin変換と、そういうのに頼らず最初からCNFを構築するための手法について検討を行います。

おことわり

自分自身、体系的に論理学を学び始めたというより、実用品としてSATに慣れ親しんでいったので、理論的におかしな所などが存在するかもしれません。そういう場合には、コメントや編集リクエストで指摘していただければ幸いです。

まず、前提知識〜2つの標準形

以前も触れましたが、SATソルバーの処理するCNF（連言標準形、Conjunctive Normal Form）は、以下のいずれかの項ををAND（$\wedge$）でつないだ形式です。あるいは、以下の3つの形の式を（典型的には複数個）与えて、それらすべてを満たす、と言い換えても本質的に同じです。

1つの変数（$A$）
1つの変数の否定（$\neg A$）
上の2つの形のものをOR（$\vee$）でつないだもの（$\neg A \vee B \vee C \vee \neg D$）

もう少し条件のゆるい標準形として、否定標準形（Negation Normal Form、NNF）があります。これは、以下のいずれかで構成されるものです。

1つの変数（$A$）
1つの変数の否定（$\neg A$）
NNF標準形の式をOR（$\vee$）でつないだもの
NNF標準形の式をAND（$\wedge$）でつないだもの

つまり、以下のものは現れません。

変数以外の項へのNOT
二重否定
ならば（$\rightarrow$）

これらについては、二重否定の除去（$ \neg\neg A \Longrightarrow A$）、「ならば」の定義に沿った変換（$A\rightarrow B\Longrightarrow \neg A \vee B$）、ド・モルガンの法則（$\neg(A\wedge B)\Longrightarrow \neg A\vee\neg B$、$\neg(A\vee B)\Longrightarrow \neg A\wedge\neg B$）を使うことで、項数を増やすことなくNNFに変換可能です。これ以降では、NNFになった状態の論理式だけ考えます。

分配法則…だけでは捌けない

NNFをCNFに直すには、ORとANDが入り組んだものをどうにかする必要があります。いちばんシンプルな方法としては、「分配法則」を使う、という方法があります。

\begin{align}
A \wedge (B\vee C) &= (A\wedge B)\vee(A\wedge C) \\
A \vee (B\wedge C) &= (A\vee B)\wedge(A\vee C)
\end{align}

このように、ANDとORを内側と外側で入れ替えることができます。これを使えば、すべてをCNFに持っていけそうな気がします。それは実際に可能ではあるのですが、1つの問題があります。

\begin{align}
(A\wedge B) \vee (C\wedge D) &= (A\vee (C\wedge D))\wedge(B\vee (C\wedge D)) \\
&=(A\vee C)\wedge(A\vee D)\wedge(B\vee C)\wedge(B\vee D)
\end{align}

というように、項数が増えてしまいます。このくらいであればどうということはないのですが、AND2つの項を100個ORでつないであるような場合、合計の項数は $2^{100}$ となってしまいます。これでは計算不能です。

変数を増やして条件を書きやすく…Tseitin変換

もちろんこのままではSATへたどり着けませんので、どうにかしないといけません。そこで取る戦略として、「Tseitin変換」という手法があります。これは、

新しい変数を1つ作って、内側の式をその変数に置き換える
いちばん外側の条件として、「置き換えた変数=元の式」となるように条件を追加する

という方法です。変数は増えますが、機械的に行える上に項数が爆発的に増えることもありません。

内側のANDをくくり出す

では、一例として、$A\wedge(B\vee C\vee (D\wedge E))$ をTseitin変換してみましょう。まず、新しい変数 $X$ を用意して、内側の $D\wedge E$ を$X$に置き換え、$A\wedge(B\vee C\vee X)$ とします。これで式全体はCNFの形となりましたが、このままでは$D\wedge E$の条件が反映されません。

ということで、$X\Leftrightarrow(D\wedge E)$ という条件を全体にANDしてつじつまを合わせます。これは $X\rightarrow(D\wedge E)$ かつ $(D\wedge E)\rightarrow X$ ということですが、これらを「ならば」を使わない形に直すと、それぞれ $\neg X\vee(D\wedge E)$ と $\neg(D\wedge E)\vee X$ になり、さらにド・モルガンの法則や分配法則で整理すると、それぞれ $(\neg X\vee D)\wedge(\neg X\vee E)$ と、$\neg D\vee\neg E\vee X$ というように、CNFとして表現可能な形へ変形できます。

さらに省略

じつは、NNFとなっている前提であれば、後半の $(D\wedge E)\rightarrow X$、つまり $\neg D\vee\neg E\vee X$ は省略可能です。

まず、省略しない状態で充足したとすると、ANDで結ばれた項のうち1つを省略するということは、条件は変わらないもしくは緩くなるということなので、1項省略しても当然同じ値で充足します。

逆に、省略した状態で充足したとします。「$D\wedge E$ はtrueだけど、$X$ はfalse」という状態でなければ省略した項もtrueなのでもちろん同じ値で充足します。一方、「$D\wedge E$ はtrueだけど、$X$ はfalse」だった場合には、$X$ をtrueに置き換えてみましょう。NNFなので変数以外にNOTがかかることはなく、残りはANDとORだけなので、項を1つfalseからtrueに置き換えたことで、それを含む項の値は変化しないか、falseからtrueへ変化するだけで、trueだったものがfalseになってしまうことはありません。そして、$X\rightarrow(D\wedge E)$ と $(D\wedge E)\rightarrow X$ はどちらもtrueなので、全体もtrue、つまりこれで充足されています。

つまり、「省略しない状態での充足可能性」と「省略した状態での充足可能性」は等値です。

内側のORをくくり出す

逆に今度はORを含む項をTseitin変換してみましょう。さっきと逆に、$A\vee(B\wedge C\wedge (D\vee E))$ とします。ここでも $Y=(D\vee E)$ とおくことで、$A\vee(B\wedge C\wedge Y)$ かつ $Y\rightarrow(D\vee E)$ かつ $(D\vee E)\rightarrow Y$ となりますが、先ほどと同様な議論により、（NNFでは）第3項は省略できます。そこで第2項だけ変換していくと、 $\neg Y\vee D\vee E$ となります。

ANDとORが複数入り組むような複雑な式でも、内側から順にTseitin変換していけば、最終的にはCNFへ変換できます。

最初からCNFを立てるための考え方

Tseitin変換は機械的にできるので、もちろんそれに任せてもいいのですが、変換せずに最初からCNFを立てられればそのほうが便利です。もちろん、結局は追加変数が必要になることもあるのですが、考え方を変えれば最初からCNFにできることも多々あります。

例えば、ある条件 $A$ が、「『複数の変数やその否定』をANDした項」をORでつないだものになったとします。状況によっては、その否定の条件 $\neg A$ も、同じように【「『複数の変数やその否定』をANDした項」をORでつないだもの】で書けることがあります（とりわけ、a＞bのような不等号を条件としていた場合、否定してもa≦bとなって、同様の形で書けるケースが多いです）。

そうなればしめたもので、この $\neg A$ をさらに否定すれば、【「『複数の変数やその否定』をANDした項」をORでつないだもの】の否定、ド・モルガンの法則で変形すれば【「『複数の変数やその否定』をORした項」をANDでつないだもの】となり、これはすなわちCNFの形です。