minisat という SAT ソルバの ruby バインディングを作ってみました。1.8.5 と 1.9.0 で動作確認してます。
http://dame.dyndns.org/misc/misc/ruby-minisat-1.14.0.tar.bz2
例えば という SAT 問題を解くときはこんな風にします。
require "minisat" solver = MiniSat::Solver.new # 問題定義 a = solver.new_var b = solver.new_var solver << [a, b] << [-a, b] << [a, -b] # 解の探索 p solver.solve #=> true (satisfiable) # 解の表示 p solver[a] #=> true p solver[b] #=> true
リテラルの配列で表現した clause を MiniSat::Solver にどんどん追加していく感じです。
これを使って、数独、スリザーリンク、お絵かきロジック、カックロ、ナンバーリンク、四角に切れなどのソルバも作ってみました。それぞれのパズルのルールや盤面を SAT 問題に変換して SAT ソルバに解かせ、得られた解をパズルの解答に逆変換して表示するプログラムたちです。example/ に入れてあります。どれも普通サイズの問題なら一瞬で答えが出ると思います。お試しください。
minisat を含む世の SAT ソルバは驚くほど速いです。真に速いソルバは各問題に応じてプログラムを書かないと得られないでしょうが、大抵の人が下手に自力でソルバを書くよりは、SAT 問題にエンコードして SAT ソルバに解かせた方が (動作速度的にも開発速度的にも) 速いです。上記のソルバたちはそれぞれ数時間〜二日くらいで作れました。ruby-minisat なしだと動作速度の問題から Ruby は使えませんし、Ruby を使ったとしても開発だけでもっと時間がかかりそうです。
ただし、解きたい問題を SAT 問題に変換するにはちょっとコツが必要です。上記の各パズルをどうやって SAT にエンコードしているかはコメントに (怪しすぎる英語で) 書いてありますが、そのうちブログでも紹介したいと思います。
Todo:
