僕が勉強したときはwikipedia(en)とこの記事を参考にさせていただきました。
ここでは
変数 : xのこと.今回はa,b,cとかx,y,zとかで表す。
リテラル : x、!xのこと
Boolean function :ここでは and, or , →, notで構成された式のこと.変数に0か1を代入すれば0か1が返ってくるとする。φで表す。
DNF : リテラルをandでつなげたものをorでつなげてできたBoolean functionのこと
CNF : リテラルをorでつなげたものをandでつなげてできたBoolean functionのこと
clause : リテラルをorでつなげたもの。CNFはclauseをandでつなげてできたものと言い換えることができる。
Boolean functionのサイズ : 文字列としたときの長さ
二つのBoolean functionが等価 : 任意の割り当てに対して同じ値が返ってくること。
充足可能性問題(SAT) : 与えられたBoolean functionが1を出力するような割り当てがあるかどうかを判定する問題。NP-completeである。
とします。サイズの定義に関しては変数の個数とかそういうのもありますけどどれも結局linearの関係にあってオーダー的には成り立つので今回は文字列長としておきます。
任意のBoolean functionを等価なDNFもしくはCNFに変換しようとすると、変換後のCNFは元のサイズの指数長になりえます。しかし例えば充足可能性を問題にしている場合には
φが充足可能 ⇔ φ' が充足可能
となるような変換であれば良いわけで、等価である必要はありません。今回紹介するTseitin transformationというのを使うと「充足可能性を保存して、かつ元のBoolean functionの線形オーダーのサイズであるようなφ'」を得ることができます。おそらく例を見るのが一番わかりやすいと思います。
例 :
充足可能性を保存するような変換をすると
こんな感じになります。p⇔qというのは要するにpとqが等しい値をとれば1を返すような論理関数です。(xorの否定)
イメージ的には連立方程式みたいなものだと思っています。
最後にそれぞれの()の中身を等価なclauseに変換してやればオッケーです。この作業は分配法則とか使ってうにゃうにゃやればできるはずです。こうして得られたものは確かにCNFになっているし、サイズも指数的に増えていません。変数が増えているために等価にはなっていないのですが、a,b,c,dがφを充足するときはそれぞれのv,w,x,y,zを()の中と等しい値にしてやればφ'は従属されるし、逆にφ'を従属するような割り当てa,b,c,dはφを充足します。つまり充足可能性を保存しているわけです。
分かってから見れば当たり前なのですが新しい変数をおくという発想は面白いと思いました。
