情報処理学会 第78回全国大会講演要旨

近年著しい高速化がなされているSATソルバーは幅広い制約問題に応用できる基礎技術である。そのため各種言語においてライブラリとして実装がされている。
最適化コンパイラを持つ関数型言語Haskellにおいてもいくつかの実装が存在するが、代表的なSATソルバーであるMinisatの実装に関する論文を参考にしたものであっても、Minisatと比較して大きな性能差があるという現状である。我々はこのギャップを埋めるためにMinisatの実装を再度行い、性能差の原因を調査した。その結果、ヒープメモリ使用量、多相性によるオーバーヘッド、等価性の判定などに問題があることがわかった。論文ではこれらの問題点の解消の効果について報告する。