Hatena::ブログ(Diary)

まめめも このページをアンテナに追加 RSSフィード

2008-01-06

[] ruby-minisat とパズルのソルバ

minisat という SAT ソルバruby バインディングを作ってみました。1.8.5 と 1.9.0 で動作確認してます。

http://dame.dyndns.org/misc/misc/ruby-minisat-1.14.0.tar.bz2


例えば (a ¥vee b) ¥wedge (¥bar{a} ¥vee b) ¥wedge (a ¥vee ¥bar{b}) という 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:

  • ちゃんとドキュメントを作る (rdoc minisat.c で一応それっぽいものはできます)
  • ちゃんとリリースする (rubyforge とかで)
  • 割り込みをどうにかする (今は solve 中はブロックします。他の Thread も動きません)
  • minisat の内部状態がわからなくてデバッグしにくいのをどうにかできたらいいなあ

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証