Kissat2024sc

 Armin Biere教授のKISSATが優勝しました。Paperは、

https://kfazekas.github.io/papers/BiereFazekasFleuryFroleyks-SAT24.pdf

解いた数は、殆ど変化はありません。しかし、解くスピードがイノベーションです。

問題をどのようにCNF化するか、というのは、一意ではなく、知識や経験においてSATソルバが解きやすい形態にすることは重要です。その意味において、ベンチマークインスタンスは、必ずしも最適な形態ではないので、その辺を解きやすい形に変換することがポイントだと思います。言い方を変えると、私のようにSATソルバの特性に熟知した人がモデル化したCNFとそうでない人がモデル化したCNFでは差があり、そのようなインスタンス群に対して効果がある手法だといえます。

今年のクラウドや、パラレルトラックについては、特に見るべきものはなく性能向上は誤差の範囲内だと思います。