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 リテラルの配列で表現した clau
数独は非常に SAT に変換しやすい問題です。全部参考文献 *1 に載っている内容ですが、なるべくわかりやすく説明してみます。ちょっと長いです。 SAT とは まず SAT をごく簡単に説明します。すでに SAT を知っている人はここは読み飛ばしてください。 命題論理式の形の一つに乗法標準形のというのがあります。変数か変数の否定 (リテラルと言います) を or だけでつないだ式 (節と言います) を and だけでつないだ論理式のことを言います。つまり以下みたいな形です。 ( a1 or !a2 or ... or an) and ( b1 or !b2 or ... or !bn) and ... and (!z1 or z2 or ... or !zn)SAT は「a1 や zn などの変数にうまく true か false を代入して、上の式全体を true にできるか」という問題
奥村晴彦さんの「C言語による最新アルゴリズム事典」技術評論社、1991年、の C 言語プログラムの Ruby への翻訳に挑戦します。プログラムの説明は同書を読んでください。変換はできるだけ逐語的に行っています。プログラムの動作は原作の C プログラムのそれと比較してチェックしていますが、うまく動作しないときは C から Ruby への変換のさいに起きたものです。バグレポートは tnomura@mnet.ne.jp までお願いします。 この Ruby 翻訳版はできるだけレイアウトも含めて原作の C プログラムを変更しないようにしたため、必ずしもRuby らしいコーディングスタイルとは言えないかもしれませんが、プログラムがきちんと動作することを優先しました。C から Ruby への翻訳の著作権に関しては Ruby のライセンスに準じます。配布、改変は自由です。ただし、プログラム本体には原作者の
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
