DPSの移植失敗

 山梨大学鍋島先生のDPSに最新版KISSATをWindowsに移植しようとしたのですが、失敗しました。原因は良くわからず、断念しました。

DPSは、パラレル版のソルバで、Determisticという特徴がありながら、性能劣化を極小にしているところが素晴らしいです。

DFS: A Framework for Deterministic Parallel SAT Solvers

最新版のKissatは、長い時間でみるとあまり性能向上はないのですが、短い時間でみると効果があるようです。なので、是非組み込みたかったのですが、何か見落としがあるのだと思いますがパラレルにするとクラッシュしてしまう問題が発生しました。

とりあえず、sc2021時点のkissatでのWindowsポートは出来たので、これから評価してみたいと思います。上手く組み込みできれば、求解毎のバラつきを抑えることが出来る筈です。勿論、そのままでは組み込み出来ないので、色々やることはあるのですが、基本性能は、SAT能力で決まり、機械的な手順でスケジュールナースのメインソルバとして使うことは出来る筈です。今後の予定としては、Algorithm５として実装予定で、リノベーション後のAlgorithm3/4でも使用予定です。