最新のSATサーベイ

こちらのIntel　NadalさんのlectureNoteが分かりやすいです。 

SAT/SMT/AR/CP Summer School 2022 (sat-smt-ar-school.gitlab.io)

Kissatのパフォーマンス向上が最近ではトピックになっています。背景として、CDCLにローカルサーチを組み込んだことが大きいのではないかと思っています。論文は、

Deep Cooperation of CDCL and Local Search for SAT

こちらもparallel satの覇者Shaowei Cai教授によるものです。この方は、私が競技会に参加していた頃から、ローカルサーチ手法を用いて参加していました。当時、評価したものの、利点はあまりなかったように感じましたが、ここに来て長年の研究が実を結んできたように思います。

しかし、Kissatもそうですが、incremental solvingに対応していないので、使用しづらい面があります。そこで、最近の成果を盛り込みかつincremental なSATということで、NadalさんIntelSAT等を使用することも考えられます。

しかしながら、最近の成果は、optimization problemには、効果がない、というNadalさんの指摘もあります。

が、来年以降、並列SATの分野で、性能向上が見込めます。そこで、ここ2-3年の成果を取り込んでマルチプロセシング向けの基幹系を実装しておくことは意味があると思います。