ベンチマーク問題INRC2 n110w4_0_1-4-2-8を解く途中に出現するSAT問題を用いて性能比較しました。
ヒントの数が多ければ多いほど解くのが容易となる傾向にあります。ヒントのサイズ、Fixed Lits Sizeをパラメータとしたとき、何秒で解けるかを評価したものです。
ソルバは、CADICAL最新版、KISSAT去年、KISSAT今年、DPS去年、PRS今年のSAT competition提出版になります。DPSとPRSは、32threadsのパラレル版で、いずれもその時点のKISSAT最新版がベースになっています。
青が1位、黄色が2位でマークしています。一見して分かるのは、
■パラレル版が10倍程度高速で安定傾向、PRSが最速
■SAT Solver Single thread版でも最新になるほど性能向上が見られる
さらに考察として、
PRSに搭載されているKISSATは、去年以前のKISSATがベースですから、今年のKISSATにReplaceすれば、さらに性能向上が期待できます。
しかし、ヒントの数が少ないと、PRSをもってしても現実時間内に解くことは出来ません。（1割少なくなっただけで、もはや解くことが出来ません。ヒントなしでは論外。）
つまり、SATソルバだけでは解くことは出来ないことを示しています。一般に、解空間が広い場合（最適化の結果、残る解の個数が多い場合）SATソルバのみで解くことが出来ますが、INRC2問題のように解空間が非常に狭い最適化問題の場合は、複合技が必須となります。今回の問題で言えば、SATソルバを選ぶことに注力するより、ヒントの数を増やした方が遥かに効率的に解くことが出来ます。
今回、パラレル版で意外な性能向上が見られたので、採用しようかな、と思います。今回求めているのは、UNSAT証明能力で、SAT解探索能力と比例傾向にあるからです。
