KISSATの衝撃

 SAT Competition2020の結果をよくみると、KISSATが突出した性能を備えていることが分かります。で、2022以降、全てKISSATベースのソルバが上位を独占することになります。これは、CHB以来の衝撃ではないでしょうか。数理ソルバの実装をしている間に、SATの進歩がありました。

理由の一つとして、ローカルサーチかな位に考えていたのですが、主因は、メモリ消費量だろうと考えを改めました。というのも、KISSATのメモリ消費は、1/３から1/4になっており、キャッシュヒット率の向上というのが貢献していることが理由です。MINISAT以来、伝統のClause構造体を一新しており、その複雑怪奇な構造変更が、2年経っても、未だincremental ソルバが出てこない理由ではないかと推察しています。

A)SATパラレルの問題点は、コアを増やしても性能が向上しないばかりか劣化することです。この点でmerge_satや、DPSは、決定的なソルバであり、コア数が決定されれば、性能は安定していますが、予備実験によれば性能向上は期待したほどではありませんでした。

B)最適化を行うには、incremental機能は不可欠です。Kissatのソースを期待を込めて読んでみたのですが、ソース上は対応していませんでした。(option でincremental指定はありますが、ソースを見ると対応していませんでした。）

ここ2-３年のSAT性能の向上を取り入れることによりAlgorithm1をReplaceすることを計画したいと思います。目標は、

■　マルチコア時の安定した性能向上

です。既にAlgorithm1は、他と比べて圧倒的な性能を有していますが、マルチコア時に難がありました。　数理ソルバの実装には、数年を要したのですが、この分野は自分の専門領域でもあり、一月程度で結果は出せると思います。