年末新年を気持ちよく迎えるために

SATソルバの性能を議論する唯一の指標はSAT competition で使われている400問のベンチマークの求解数だけだろう。 しかしその評価は膨大な計算機リソースを必要とし、正直なところ個人ベースでは現実的でない。なので、これまでは外挿可能だろうという楽観的な見通しの下、極めて短いタイムアウトを設定して実験を繰り返してきた。さらにその前段のスクリーニングとして SAT-bench による3-SAT問題中心のマイクロベンチマークを実行して、合計実行時間の短縮と短いタイムアウト時間内での求解数の向上とを改善指針にしてきた。

しかしこれは過学習の危険性が避けられない。これまではこの問題は敢えて無視してきたけど、泥沼のようなパラメータチューニングはそれでも避けられないため、ちょっとしたパラメータチューニングのつもりで始めた改良ですら二ヶ月が経ってしまう。そしてこの実験に追われて、SAT Competition ベンチマークの対象を今年のものに変更することすらできてないという惨状。

この状況は変えよう。SAT Competition ベンチマークの結果が悪くてもリリースできるような指針を作って行こうと思う。

3-SATで高速な設定がSAT Competition ベンチマークでの好成績に全く結びついていない以上、SAT-bench での評価指針は （今までやってきた）合計実行時間の最小化ではなく、もっと大幅に延長したタイムアウト時間内での求解数、そしてその最悪問題の実行時間の最小化としてみたらどうだろうか。 これは 解ければ必要時間は気にしない という方針に沿うものになっているのではなかろうか。 そして、この値が改善できれば、SAT Competion ベンチマーク（それもタイムアウト時間が正式ルールよりも大きく短い）の結果が悪くても新バージョンとしてリリースできる、と。

これが今年、1番のアイデアかもしれない。 仕事としての研究が終わってからようやく研究マネージメントの重要性を理解した気がする。