2015 Fiscal Year Research-status Report
SAT符号化を用いた制約解集合プログラミングに関する研究開発
| Project/Area Number |
15K00099
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
番原 睦則 神戸大学, 情報基盤センター, 准教授 (80290774)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
田村 直之 神戸大学, 学内共同利用施設等, 教授 (60207248)
宋 剛秀 神戸大学, 学内共同利用施設等, 助教 (00625121)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 解集合プログラミング / 制約プログラミング / SAT |
|---|
| Outline of Annual Research Achievements |
本研究の目的は，SAT符号化を用いて，解集合プログラミング (ASP) と制約プログラミング (CP) を融合した制約解集合プログラミング (制約ASP) を実現することである．
具体的な研究テーマは，(A) 制約ASP言語に関する研究，(B) 制約ASPソルバーの設計・実装，(C) 制約ASPソルバーの拡張，(D) 制約ASPの特長的なアプリケーションの開発，および問題記述例の蓄積の4つである．
本年度は，上記の(A)と(B)を中心に研究開発を進めた．海外共同研究者・Schaub教授 (ポツダム大学，ドイツ)と協力して制約ASP言語の設計を行い，制約ASPソルバーclingconを実装した．この研究成果については，国際ジャーナル論文に投稿中である．また，制約充足問題(CPの言語)をASPに符号化し，既存のASPソルバーで求解するCPソルバーAspartameを実装した．このAspartameは，制約充足問題をSATに符号化する順序符号化法を応用したものであり，既存のSATベースの高速CPソルバーSugarとほぼ同等の性能を実現した．この研究成果については， 国際会議LPNMR2015で発表した．さらに，制約充足問題をSATに符号化する新しい方法として，順序符号化法と対数符号化法を融合したハイブリッド符号化を提案した．このハイブリッド符号化は，順序符号化法と比較してより大規模な制約充足問題を取り扱えることから，今後のAspartameの実装・拡張において重要な役割を果たすことが期待できる．この研究成果については，国際会議ICTAI2015で発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究は交付申請書に記載した「研究実施計画」に照らして順調に進捗している．(B)の制約ASPソルバーの設計・実装には，大きく分けて「SMT型」と「符号化型」の2つがある．現時点でどちらの方法が優れているかの判断は難しい．そのため，本研究では両者の長所・短所を詳しく研究調査し，両者のハイブリッド方式も視野に入れつつ研究開発を進めることが重要となる．実際，本年度開発した制約ASPソルバーclingconは「SMT型」，CPソルバーAspartameは「符号化型」を採用している．新しく考案した制約充足問題からSATへのハイブリッド符号化法は，「符号化型」のための最適化技術として有用である．
次年度以降に計画されている(C)制約ASPソルバーの拡張，(D) 制約ASPの特長的なアプリケーションの開発および問題記述例の蓄積について，その準備として以下の研究を行った．「組合せテストケース生成問題に対する制約解集合プログラミングの適用」と題する研究発表を2015年度人工知能学会全国大会(第29回)で行い，全国大会優秀賞を受賞した．また，制約最適化問題をSATソルバーのインクリメンタル解法を用いて効率良く解く方法について研究開発を行った．この研究成果は，日本ソフトウェア科学会論文誌コンピュータソフトウェアに採録が決定している．さらに，開発したソルバーは，アルゴリズムデザインコンテスト(情報処理学会DAシンポジウム2015の企画イベント)において，第1位となり最優秀賞を受賞した．
|
| Strategy for Future Research Activity |
中間年度である平成28年度は，(A)の制約ASP言語に関する研究を終え，(B)の制約ASPソルバー開発を完成する．また，(C)の制約ASPソルバー拡張を開始するとともに，(D)の制約ASP記述例の蓄積についても着手する．(C)では，インクリメンタル解法，ヒューリスティクス埋込み機能等の高度なASP解法を利用することにより，(B)で開発した制約ASPソルバーを拡張する．この拡張により，モデル検査をはじめ近年様々な分野に応用されているCEGARループ，CPの分野でこれまで研究されてきた変数選択および探索ヒューリスティクスなどを，簡潔に記述できるようになることが期待できる．
最終年度である平成29年度は，(C)の制約 ASP ソルバー拡張，(D)のアプリケーション開発および問題記述例の蓄積を完成する．そして最後に，(D)の問題群を用いて，(B), (C) で開発したソルバーの総合的な評価を行う．(D)のアプリケーションとしては，時間割問題，ソフトウェアのテストケース生成問題を中心に研究を進める．特に，(C)で拡張された制約ASPソルバーを用いることにより，時間割問題に対して，主にオペレーションズ・リサーチ分野で研究されてきた様々なヒューリスティクスを利用することが期待できる．
研究代表者・番原と連携研究者・井上の研究拠点が離れているため，4名の研究者全員が参加する研究打合せを年2回開催する．ここでは，アイデア・実現技術の共有を主目的とし，進捗状況の報告，研究計画・方法に関する議論を行う.海外共同研究者はこの研究打合せに年1回参加し，本研究に関連する海外での最新動向の紹介などを通して本研究の推進に寄与する. このような密接な協力体制を整えることによって，研究が当初の計画通りに進まない場合，研究者間で対応策を検討し，研究計画・方法の見直し等を速やかに行えると考えている．
|
| Causes of Carryover |
計画当初，海外共同研究者Schaub教授 (ポツダム大学，ドイツ)との研究打合せを神戸で予定していたが，本年度はポツダム大学で開催した．そのため，Schaub教授の講演謝金が不要となり，次年度使用額が生じた．
|
| Expenditure Plan for Carryover Budget |
次年度以降の研究推進のために必要となるソフトウェア開発用パソコンの購入および旅費として使用する．
|
Research Products
(16 results)
