最近気になった論文

 CadiCaLというSATソルバの実装を見ていて、面白いインタフェースを備えていることに気づきました。案の定、SMTソルバcvc5の実装で使われているようです。

IPASIR-UP: User Propagators for CDCL - YouTube

これは、従来のスタンドアロン的な使い方に留まらず、可能性が広がることを意味しています。安直に思いつくのは、B&B(Branch and Bound)　と併用することです。その他にも可能性があり、今後の一研究領域になると確信します。

2番目の論文は、既出ですが、改めて見てみました。5%の改善ならば、最近のSAT Competitionでも優勝候補になると思います。

[2110.14053] NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks (arxiv.org)

最近、NPU搭載のCPUが出始めており、例えば、そのプロジェクトに特化した学習をオフラインで行うことが将来可能になる、というです。個別プロジェクト毎に性能向上の可能性があるということです。

しかし、上記手段を用いても速度向上は、数％のオーダでしょう。速度向上を体感できるには、2倍以上が必要と考えます。その意味で、重要なのはアルゴリズムです。新しいアーキテクチャでは、速度向上が体感できると思います。