やったこと

SATソルバ

RubyでCDCLソルバを実装した。
Scalaで実装したときよりも細かく実装したので、かなりちゃんとしたSATソルバになった。
具体的に実装した機能は以下の通り。

• DPLL
• 監視リテラル
• CDCL
• VSIDS
• LBDによるリスタート・学習節の削除

現代的なSATソルバと言えるのではないだろうか。

途中変なバグり方をしていて、claspで全部の解を列挙してあり得ないリテラルが推論されてるところを特定して原因を潰していた。
ループ内の変数の初期化忘れには注意しよう。

ヒューリスティクス周りは高速化のためというより、それが無いと現実的な時間に解けなくなるから必要なのだな、と実感していた。
とくにリスタートを実装しているときに、そういうことを考えていた。

そのうち、というか明日には公開します。