Vol.1, No.12.

UNSATlog

2020年振り返り

結局0.5.1はリリースできませんでした。12月にやったことは

リフェーズ(re-phasing to best phase)に関するチューニング
Sudoku 64への応用
Advent of Code 2020への応用

というあたり。個人的には、初めてVec以外のデータ構造(HashMap)を導入したことが大きいです。やはりリリース直前のベンチマークに時間を取られてしまったものの、ドキュメントの更新は終わっているので、ベンチマークさえいい結果、いやよくなくてもいいのでそこそこの結果が出ればリリースするつもりなので、最速で2021年元旦に出せるはず。

Best Phase Rewarding

Rephasingの実現手法として変数のrewardに反映させてみた。活性度に反映させるのではなく独立した項目にして線型結合（単に和をとるだけ）してみたら考えてみる価値がある結果になった。混ぜない方がいい。やはり合議制のマルチエージェントの並行動作が行き着くところかもしれない。全然ベンチマークでのベストを更新できてないので、これが本当によい手法と言えるかどうかは微妙なんだけど、それまでのもっとも解に近い点を足掛かりにして探索を進めるのはあるかもしれないし、まあ納得できる。意外なのは極端な設定に振った方が結果が出ていること。 Stabilizationでいえばstabilizationしっぱなしが一番いいという感じ。なので現在のコードはマルチエージェント合議制に対しては否定的なんだがエビデンスを得るためには、色々試してみないといけない。 Luby数列を使ったStabilizationとのコード的な組み合わせ爆発もあるし、なかなかこれでいいという踏ん切りがつけられない。ということで一ヶ月では終わる話題ではなかったのでした。

Sudoku 64

Sudoku 64はここで見つけたもの。 Sudoku 25が1秒以下で解けたこと、一意な解答保証のため結構初期状態で埋まったものだったことから、これもすぐ解けるのかと思ったら20秒も掛かってしまった。 BCP 始める前に解けているのでこれは pre-processor が重いのだろう。外してみると8秒でした。

$ splr --ELI 0  sudoku64.cnf
sudoku64.cnf                                262144,41048269 |time:     8.31
 #conflict:          0, #decision:            0, #propagate:         262144 
  Assignment|#rem:   259891, #ass:     2253, #elm:        0, prg%:   0.8595 
      Clause|Remv:        0, LBD2:        0, Binc: 41029632, Perm: 41037005 
     Restart|#BLK:        0, #RST:        0, Lspn:        1, Lcyc:        0 
         EMA|tLBD:      NaN, tASG:      NaN, core:   262144, /dpc:      NaN 
    Conflict|eLBD:     0.00, cnfl:     0.00, bjmp:     0.00, /ppc:      inf 
        misc|elim:        0, cviv:        0, #vbv:        0, /cpr:      NaN 
    Strategy|mode: Initial search phase before a main strategy
      Result|file: ./.ans_sudoku64.cnf
s SATISFIABLE: sudoku64.cnf

Advent of Code 2020

Advent of Codeに初参加。面白かった。 SATで解けそうな問題が2つほどあってSplrを使ってみましたが、一勝一敗。 20日目のタイル組み合わせ問題では作ったCNFが10GBを超えてしまって、Splrにロードはできたものうんともすんとも言わなくなってしまいました。結局その問題は単純にforループで回したら解けました。残念。

今後の展望

まずは0.6.0をリファクタリングバージョンとしてリリースしてしばらく勉強します。それから年2回のリリースが現実的なので5月位に0.6.0のパラメータチューニングあるいは過去のものとの再融合バージョンが出せたらいいなあ。あ、夏休みの宿題もしなければ。

Published at 2021-01-02