Parallel-Solverの進展

SAT Competition 2022でSolvers Descriptionが公開され、各Solverの概要が明らかになりました。

一位の Shaowei Cai教授が率いるグループの結果は衝撃的です。VBSというバーチャルなソルバーが解いた問題数と、実際のソルバが解いた問題数が殆ど同じ、という結果になっています。今まで、殆ど見たことのない結果です。SAT手法のありえる限界点に到達しつつあると言え、いわば自己新記録が常に世界記録となるような突出した性能を備えている、ということが言えます。

Literal Assumption and Random Shuffle

パラレルへのアプローチの仕方としては、多数の異なる求解パラメータを持つソルバ群をスレッド駆動するポートフォーリオと、問題そのものを子問題に分割するパーティションベースがあります。Shaowei Cai教授が取ったアプローチは、パーティションベースです。闇雲に分割すればよいのではなく、ある発見があったようです。crucial variablesというKeyとなるPivotが見つかったとき、あるいは見つからなくても有効なSAT手法が発見できた、ということのようです。

数理ソルバにおいてもBranchingNodeの選び方は、重要で特にRoot付近となるNodeの選出については、StrongBranchingという手法があります。数理的アプローチもSAT的アプローチも最適化を目指しているのは同じですから、未だ、今後の進展が期待できそうな分野だと思います。