2011 Fiscal Year Annual Research Report
大規模SAT問題解決のためのEPRプルーバーに関する研究
| Project/Area Number |
21300054
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
長谷川 隆三 九州大学, システム情報科学研究院, 教授 (20274483)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
藤田 博 九州大学, システム情報科学研究院, 准教授 (70284552)
越村 三幸 九州大学, システム情報科学研究院, 助教 (30274492)
力 規晃 徳山工業高等専門学校, 情報電子工学科, 助手 (50290804)
|
|---|
| Keywords | SATソルバー / 極小モデル生成 / SATソルバーの高速化 / 基数制約のSAT符合化 |
|---|
| Research Abstract |
本年度は,(A)極小モデルの全解探索を行う極小モデル生成器MiniMGの高速化手法の開発と評価,(B)SATソルバーの高速化手法の開発と評価,(C)部分MaxSATソルバーにおける基数制約節の削減手法の探求と評価について研究を進め,5件の査読付き論文の公表,3件の学会発表を行った.
以下,(A)～(C)のあらましを述べる.
(A)違反節選択ヒューリスティックに着目し,単解探索に効果的なactivity選択方式と全解探索に効果的なmin選択方式を組み合わせることにより,充足可能,充足不能,いずれの問題にも効果的な手法を開発した.また,リスタート戦略が節選択ヒューリスティックに与える影響についても実験と考察を行った.
(B)ヒューリスティクスに着目した高速化と並列実行による高速化を試みたヒューリスティクスについては,リスタート戦略,学習節の評価指標,探索手法に着目して幾つもの手法を試みた.その内の幾つかの手法については既存手法より優れていることを実験的に確かめた.並列実行については,ベースとなるSATソルバーをMiniSat2.0から2.2.0に変更し,さらなる高速化を目指した.
(C)基数制約のSAT符合化に要する節と中間変数の削減と中間変数の変数活性度を変化させ,それに伴うソルバーの性能評価を行った.また,節と中間変数のさらなる削減を目指して,詳細な検討を行い,従来の最良の手法より節と中間変数の数を減らせることを計算により確かめた.
本研究の研究成果の一つであるMaxSATソルバーQMaxSATは,MaxSAT競技会に参加し,Partial MaxSAT部門において,全14ソルバー中Industrialで優勝,Craftedで準優勝という優れた成績をおさめた.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
極小モデル生成器については,学習節の評価手法,リスタート戦略の節選択ヒューリスティックに与える影響などについて実験を行い,それぞれの特性に関して考察を行い,より大規模な問題にチャレンジできる感触が得られた.また,基数制約のSAT符合化に要する節の削減にも取り組み,巨大基数を有する問題でも対処できそうなことが分かった.以上により「大規模SAT問題解決」に向けて着実に成果が得られていると評価している.
|
| Strategy for Future Research Activity |
「大規模SAT問題解決」に向けて,大きく二つの方向を考えている.一つは省メモリ技術に関するもので,コンパクトにデータを表現することで,より高速な推論を目指す.SAT符合化の節数削減はこの方向の研究課題である.もう一つは巨大メモリ空開の有効利用に関するもので,これにより従来は全く手のでなかった問題にも挑みたいと考えている.並列実行による高速化はこの方向の研究課題である.研究成果であるソルバーを客観的に評価する場としてSAT競技会及びMaxSAT競技会を捉え,積極的に参加していく予定である.
|
