ruby-minisat とパズルのソルバ - まめめも
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) # 解の表...
http://d.hatena.ne.jp/ku-ma-me/20080106/p3
いちいちパズルにあわせたsolverをcodingするよりも、SATの式に変換するプログラムを作るほうが早いことも、という話
http://b.hatena.ne.jp/entry/http://d.hatena.ne.jp/ku-ma-me/20080106/p3
> minisat を含む世の SAT ソルバは驚くほど速いです。／大抵の人が下手に自力でソルバを書くよりは、SAT 問題にエンコードして SAT ソルバに解かせた方が (動作速度的にも開発速度的にも) 速いです。
