[2E4-OS-13c] AIと制約プログラミング(3/3)

[2E4-OS-13c-02] 圧縮した SAT 問題における高速な単位伝播手法

〇早瀬 悠真¹、鍋島 英知¹、盧 暁南¹ (1. 山梨大学)

キーワード：SATソルバー、SAT型CSPソルバー、SAT問題、SAT問題の圧縮

本研究では，圧縮したSAT問題に対する高速な単位伝播手法について実装及び評価を行う．制約充足問題(CSP)の有効な解法の一つに，CSPをSAT変換して解くSAT型CSPソルバーがある．大規模なCSPをSATに変換すると節数が数億にも及ぶ非常に巨大な問題となることがある．そのような巨大な問題はメモリに格納することが難しく，また読み込むことができたとしても処理が重たく現実的に解くことが困難である．そのような巨大なSAT問題に対して，節の圧縮表現を利用してメモリの使用量を減らす手法が提案されている．これにより，メモリに載りきらないことを原因として求解できなかったSAT問題を解けるようになったものの，求解時間や求解数に大きな向上は見られていない．本研究では，圧縮されたSAT問題のための専用の高速な単位伝播アルゴリズムを提案する．単位伝播はSATソルバーの実行時間の大部分を占める基本的処理であり，これを改善することは大きな速度向上につながる．評価実験の結果，従来のソルバーよりも使用メモリ量を大きく削減するとともに，求解速度が向上し，求解性能が改善していることを確認した．