3/13に引き続き『数学ガール 乱択アルゴリズム (数学ガールシリーズ 4)』で紹介されているアルゴリズムを実際に作ってみました。今日は，第9章で紹介されている「充足可能性問題(3-SAT)を解く乱択アルゴリズム(p353)」です。
rw3sat.rb
- 5行目
- 36行目で生成した論理式をandで分割。配列ffにはクローズが格納される。
- 8行目
- x[0], x[1], x[2], x[3]にtrue, falseを割り当て
- 11行目
- それぞれのクローズを評価し，全て真なら"充足可能である"と出力
- 12行目
- 充足しないクローズを覚えておくための変数c
- 13〜18行目
- それぞれのクローズを評価し，充足しないクローズ(cc)が出てきたら，cに代入しeachブロックを抜ける。
- 19行目
- クローズから数字部分を抜き出し(scan)，乱択(sample)。
- 28〜35行目
- p336の[問題9-1]のP1〜P8を設定。強正美優がそれぞれx[0],x[1],x[2],x[3]に対応
- 36行目
- クローズから論理式(3-CNF)を生成
- 38行目
- randam_walk_3_sat関数の呼び出し
実行結果
$ ruby rw3sat.rb おそらく充足不可能である
追記
- @antimon2 さんがRubyで短くしてくださいました。本に合わせるために，timesはあえて使わなかったのですが，10行目のfindは勉強になりました。
- @omasanori さんが「複数のクローズを充足しない場合にどのクローズを選択すればいいか」とツィートされていたのを見て，以下のように変更しました(W10の部分)。もとのは，最初に見つかったクローズをただ選択していただけなので…。
