[1E2-OS-3a] AI における離散構造処理と制約充足(1)

[1E2-OS-3a-02] SATソルバーGlucoseを用いたMCS列挙

〇越村 三幸¹、佐藤 健² (1. 九州大学、2. 国立情報学研究所)

キーワード：充足可能性判定、MCS列挙

解を一つも持たない制約集合のMSS（Maximal Satisfiable Subset）あるいは
MCS（Minimal Correction Subset）を求めることは，人工知能の様々な分野で
重要とされている．本稿では，SATソルバーを利用したMCSの列挙を論ずる．
同様の研究は多くあるが，我々は，効率性の点でそれらを上回る
列挙手続きの提案と実装を目的としている．
本稿ではその基本手続きを示し，その実装の性能を現時点で最高性能を示していると思われ
るEnum-ELS-RMR-Cacheと比較した．
この結果，提案手法はPMSに対しては優位であったが，MSに対しては劣っていることが分かった．