From Gameplay to Symbolic Reasoning: Learning SAT Solver Heuristics in the Style of Alpha(Go) Zero https://arxiv.org/abs/1802.05340 CDCL SATソルバにおける変数のブランチのヒューリスティクスを機械学習ベースのものに置き換えたら、少ないブランチ回数で解けた話。

自分が https://plus.google.com/+MasahiroSakai/posts/2eqZjLqMz59 で考えていたものに近い。 ベースラインのVSIDSは速度を優先した簡単なものなので、より賢いものに置き換えれば（実時間はともかく）ブランチ回数は減らせる余地はありそうではあったけれど、それをちゃんと確認できたのは意義があると思う。

一方で現在の状態をどこまでモデルに突っ込んでいるのかがちゃんと書かれていないので、これだけ読んでもよく分からない。 それに、VSIDSをVSIGSとtypoしてるし……