| 研究概要 |
本年度は,(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で準優勝という優れた成績をおさめた.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
極小モデル生成器については,学習節の評価手法,リスタート戦略の節選択ヒューリスティックに与える影響などについて実験を行い,それぞれの特性に関して考察を行い,より大規模な問題にチャレンジできる感触が得られた.また,基数制約のSAT符合化に要する節の削減にも取り組み,巨大基数を有する問題でも対処できそうなことが分かった.以上により「大規模SAT問題解決」に向けて着実に成果が得られていると評価している.
|
| 今後の研究の推進方策 |
「大規模SAT問題解決」に向けて,大きく二つの方向を考えている.一つは省メモリ技術に関するもので,コンパクトにデータを表現することで,より高速な推論を目指す.SAT符合化の節数削減はこの方向の研究課題である.もう一つは巨大メモリ空開の有効利用に関するもので,これにより従来は全く手のでなかった問題にも挑みたいと考えている.並列実行による高速化はこの方向の研究課題である.研究成果であるソルバーを客観的に評価する場としてSAT競技会及びMaxSAT競技会を捉え,積極的に参加していく予定である.
|
