Vol.1, No.6.

6月の総括

先月、性能良くなってきたのでなんとかかんとかと書いたのですが、実はGlucose 4.1よりも全然改善されてないことがわかったので、前言撤回。どうしたものか半分途方にくれた6月でした。 後半は気を取り直して、vivificationの実装に取り組みました。

Vivification

読んだのは2008年の論文。

• C. Piette, Y. Hamadi, and L. Saïs, "Vivifying propositional clausal formulae," Front. Artif. Intell. Appl., vol. 178, pp. 525–529, 2008.

短い論文だったし、アルゴリズムもそれほど難しいものではなかったので一週間程度でできたけど、まあ遅い。 計算量的に確かにそうならざるを得ない。ちょっと色々と改良した後で2018年の論文を読み出した。

• C.-M. Li et al., “Clause Vivification by Unit Propagation in CDCL SAT Solvers,” 2018.

まだ途中を読んでいる所だけど、もう一捻りしないといけないのは確かなようだ。 ということで今年の夏も黙々と実装を続けることになりました。 ああイベント参加したかった。

なお、この実装中にeliminatorのタイマー設定が大きすぎていたことが判明。 実はこの修正のおかげで求解数が少し増えました。

おわりに

と、これでおしまい。この夏はコーディングよりも頭を使う期間かもね。