Machine Learning-Based Restart Policy for CDCL SAT Solvers https://link.springer.com/chapter/10.1007/978-3-319-94144-8_6
SATソルバでリスタートが何故性能向上につながるのかの仮説の検証と、それに基づいた機械学習ベースのリスタート方策の提案。
前者に関しては、これまで乱択での実行時間の分布の裾の重い部分を引いてしまったのを回避できるという仮説などがあったけど、ここではリスタートが割当スタックをコンパクト化することを通じて、良い節が学習できているからという仮説に立っている。この仮説を検証するために、リスタート間隔の短さとコンフリクト時の割当スタックのサイズの相関、割当スタックのサイズと(良い節の尺度である)LBDの短さの間に相関があること、LBDの短さと(リスタートに要する時間を除いた)ソルバ時間の短さの間の相関を実験的に確認。
これに基づいて機械学習ベースのリスタート方策として、過去のLBDの系列から次のLBDを予測して、それがLBD分布の99.9%分位点を超えていたらリスタートするという方策を提案。 LBDの真の分布は分からないので過去のLBDから正規分布で近似、次のLBDの予測に関しては過去の3回のコンフリクトのLBDを用いた二次多項式回帰なんだけど、コンフリクトの度に全データを使って回帰をし直すのではなく、新しく得られた1サンプルだけを使ってAdamを1ステップ実行する形で学習していく。
実装はGlucoseを改造して実装。 性能的にはLuby数列を用いたリスタートよりは良いが、Glucoseのデフォルトの方策（直近50コンフリクトの平均×定数(デフォルト0.8) が全LBDの平均を超えた時にリスタート）よりは悪いという結果（その間くらい）。
accepted papers のリストが出た時にタイトルから連想したものとはちょっと違ったけれど、面白かった。
あと、スライドの方には Research Question (RQ) と書いてあるけれど、ソフトウェア工学系の論文以外で RQ と書いてあるの初めてみたかも…… (^^;
スライド https://easychair.org/smart-slide/slide/nTSR
ソースコード https://sites.google.com/a/gsd.uwaterloo.ca/maplesat/mlr
#ns
Machine Learning-Based Restart Policy for CDCL SAT Solvers
