SATヒューリスティクスの歴史

 長い間、VSIDSというスコアリングが主流でした。その後MapleSATでLRB、その実用形態としてCHBが提案されました。KISSATではCHBは実装されず、またCryptiminisatでも廃止に至ってまたVSIDSに回帰しています。しかし、その後、MABとして、ダイナミックに切り替える方法が提案されて現在に至ります。

ConstraintSolving[2]SATSolvingBasisAndCDCLpdf (ios.ac.cn)

アルゴリズム１系も見直すにあたり、ヒューリスティクス系も見直すことにしました。

SAT　Solverを牽引してきたのは、フライブルク大学のArmin Biere教授です。

paper6.pdf (ceur-ws.org)

MiniSAT以来、色々提案はされていますが、Kissat以降目立った向上はありません。