SATソルバを使うためにCNFを作る

SATソルバっていうのは，充足可能性問題（SATisfiability problem）を解いてくれるソフトウェアのことで，SATソルバで数独を解くとか，以外と身近なところに応用があったりします．SATソルバは数独を解くだけじゃなくて，プログラムの停止性の判定に使うとか，いろいろな応用を考えることができる良いものです．普通，SATソルバはCNFという論理式の特殊な形を取り扱います．日本語だと乗法標準形とか言うらしいですけど，別にこの言葉は忘れても良いと思います．詳しくはWikipediaでも見てもらえれば良いのですが，CNFは，変数かそのnot付けたやつ，をorで結んだやつ，をandで結んだやつ，という意味です．

  • CNF ::= c1 && ... && c2
  • c ::= l1 || ... || l2
  • l ::= x | !x

任意の論理式(変数(x)とor(||)とand(&&)と「ならば」(→)と否定(!)を使ってできるやつ)は，意味の等しいCNFに変換できることが知られています．そういうわけで，問題を「適当な論理式が充足可能かどうか」で表現できれば，ちゃちゃっとCNFに変換して，それをSATソルバを使って簡単に問題を解くことができることがわかるわけです．

やったね！


と言いたいところですが，CNFを作るまでに一苦労した人がいるとかいないとか言うのが今日のテーマです．

あんまり賢くない子のやりかた

CNFを作るのは，だいたいこんな手順で行います．

  1. ならば（→）を取り除く（P→Qと!P || Qが等しいのは常識ですよね）
  2. 否定（!）を変数に付くところまで，内側に移動させる（ドモルガンの法則を思い出しましょう）
  3. (A&&B)||Cみたいなやつがあったら，(A||C)&&(B||C)に変換します

できたー．

なんとなく3番目の規則が嫌ーな感じがしますが，とりあえずためしに，

(x1 && x2) || (y1 && y2)

みたいな論理式をCNFに変換してみるとどうなるでしょうか．

(x1 || y1) && (x1 || y2) && (x2 || y1) && (x2 || y2)

みたいな感じになりますね．全部の組み合わせを&&しないといけないので，すげー嫌な感じです．

つまりこいつが問題です．||の右側やつのサイズをn，左のサイズをmとすると，変換後はn*mのサイズになります．n=100だと，10000になります．変数が10000個とかいまどきのSATソルバにとっては誤差の範囲ですが，あんまり賢くない子のCNF変換にとっては大問題です．手で書くとそんな大きな問題は出てきませんが，機械的に論理式を作るような場合は，簡単に（CNFが）アホみたいなサイズになってしまいます．それでもいまどきのSATソルバにとっては（以下略）とにかく大問題なんです．

どのくらい大問題になるかというと，すぐにメモリが足りなくなって，GCしまくりになって全然処理が進まなくなって，とりあえず実行を始めてからあんまり終らないので，お昼ごはん食べに行って，帰って来ても終ってなくて，タバコ吸いに行ったり，コーヒー飲みにいったり，だらだらしても終わらなくて，泣く泣く夕方になってCtrl-Cでプログラムを強制修了させるくらい，終わらなくなります．SATソルバ，起動すらしてねえ！要するにGCが終わらないのが問題なので（間違い！）imperativeにメモリを再利用できるようにプログラムを書き直したらバグったりとか，False && x && ...みたいな式があったらSATソバル通すまでもなくFalseじゃんみたいに枝刈りやってみたりとか，そういうのをやっても全然問題は改善ません．

もうPrologを使うと20行でSATソルバが書ける時代にCNFが作れないとか，許されません．ああ困った．

ちょっと賢い子のやりかた

実は問題は"等価（equivalent）なCNF"を作ろうとしたことにあります*1．CNFを作って何がしたいのか考えてみると，充足可能性を検査したいだけなので，実は等価である必要はありません．equi-satisfiableで良いのです．つまり充足可能性が保存されていれば，等価である必要はありません．

これを踏まえて考えると……と言うか，考えた人が昔いて，CNFに変換したときの論理式のサイズの増大を線形に抑えるような方法が知られています．Tseitin Encodingとか言います．Tseitinって何て読めば良いのかわからないので，口にはしないようにしています．

Tseitin Encodingっていうのはこういう感じです．

  1. 式がA&&Bだったらxに置きかえる．ただし，xは新しい変数で，x ⇔ A'&&B'であるとする．ここでA'とB'はAとBをTseitin Encodingしたもの
  2. 式がA||Bだったらxに置きかえる．ただし，xは新しい変数で，x ⇔ A'||B'であるとする．ここでA'とB'はAとBをTseitin Encodingしたもの
  3. 式がA→Bだったらxに置きかえる．ただし，xは新しい変数で，x ⇔ A'→B'であるとする．ここでA'とB'はAとBをTseitin Encodingしたもの
  4. 式が!Aだったらxに置きかえる．ただし，xは新しい変数で，x ⇔ !A'であるとする．ここでA'はAをTseitin Encodingしたもの

こんな感じで．最終的にTseitin Encodingした結果の式（変数になりますが）と新しく導入した変数と論理式の対応（x ⇔ y && zみたいな形の集合）の組をCNFに変換してあげればよろしい．x⇔Pはx→P && P→xと等しいので，そうやって変換して，それぞれをCNF変換した後で，&&で繋げてあげれば大丈夫です．

こうすると，CNF変換の結果はlinearにサイズが増えることになるのでまあそれなりのサイズにはなるのですが，あんまり賢くない子のやりかたはexponentialなので，はるかにマシです．めでたしめでたし．


equi-satisfiableでequivalentではないのは，もとの式に含まれていない変数が導入されているあたりで，元の式の充足可能性だけを考える場合には，新しい変数の値はなんでも良い，ってことです．(x||y)&&zをTseitin Encodingするとa，a ⇔ b&&z，b ⇔ x||yになるんですが，bはFalseで！とか言っちゃうと，Encodingした後の式は充足可能じゃなくなります．でも元の式にはbとか出てこないんで，別に平気．

まとめ

  • SATソルバを使うには，論理式をCNFという形式に変換する必要があります
  • naiveなCNFへの変換は，exponentialに式のサイズが増えて，変換が終わらないなんていう悲しいことになります
  • Tseitin Encodingを使うと，式のサイズの増分がlinearになるので，変換が終わるようになります
  • 実装はRubyで書いてみたんですが，思ったより長いので省略
  • "Decision Procedures: An Algorithmic Point of View"みたいな教科書とかに書いてある話です．Googleブックスで読めるみたい．12ページとかに書いてあります．

あとがき

チュニジアで一月インターンシップやってた時にSATソルバを使ったのですが，そのときにCNFへの変換が終われなくて困りました．要するに教科書に書いてある話なので教科書があるか，せめて私がTseitinとかキーワードだけでも覚えていれば良かったのですが，全然なにもなかったのでけっこう困りました．日本の大学で，基本的な教科書が無い研究室とかわりとありえないと思うんですが，けっこう幸せなことだと思います．

*1:等価というのは，PとQが等価というのは，Pを真にするような変数の真理値の割り当てはQをも真にし，その逆も成り立つという意味です