UltimateSolver

SC3は、複数種類のソルバを搭載しますが、どのソルバがどの系統の問題に有効かというのは、大体分かっています。しかし、どれが最適かというのは、新しい初めての問題の場合は、正直言って分かりません。そこで、全種類のソルバを一遍に走らせて、その時点の最も良い解を出せば、なにも考えずにすみます。これは、SATソルバのVirtualSolver的発想です。

SATソルバの場合は、ほぼ、同じ系統のソルバを違うパラメータで走らせるポートフォリオ戦略なのですが、ここで考えているのは、

■SAT　BASED
■UNSAT　BASED
■Meta heuristics　（Simulated Annealing)
■Numerical　Solver

です。それぞれ全く異なる性質を持つソルバですので、見かけ上の性能が良く見えるはずです。
上の4つをマルチスレッドで走らせて、その時点の最も良い解をレポートすればよいだけです。


例えば、池上先生のベンチマークは、UNSATベースで数秒で解けますが、世界に名だたるMIPソルバ、Cplexや、Gurobiでも10分程度かかります。実は、この例の方が特殊で、NurseSchedulingの場合、UNSATベースだと殆ど解けません。MIPの方がよく解けます。SATとUNSATでは、大体SATの方が良く解けます。しかし、逆の場合もあります。要は、やってみないと何が良いか分からないというのが本質的な問題です。

UltimateSolverがあれば、一挙にこの問題は解決ということになります。
問題は、それだけのソルバを揃える技術力と工数です。残念ながらSC3は、今、SATBaseの改善に全力で取り組んでいて、そこまで揃えるのは、先になります。もっと進んだ発想はそれをクラウド化
することです。こちらもAWSを視野に準備しようと思います。AWS化でご協力頂けるエンジニアの方がおられましたら、ご連絡ください。