2016 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) を完了し(C)と(D)に着手した．その結果，以下に述べる成果を得た．
(A)と(B)については，海外共同研究者・Schaub教授 (ポツダム大学，ドイツ)と協力して制約 ASP 言語の設計，制約 ASP ソルバー clingcon の実装を行い，その成果を(昨年に引き続き)国際ジャーナルに投稿中である．
(C)について，制約充足問題(CPの言語)を SAT に符号化するハイブリッド符号化の研究，SAT 問題の全解を列挙する ALLSAT の研究，制約最適化問題を解くためのインクリメンタル SAT 解法の研究を行った．これらの成果は，国際ジャーナル(2本)と国内ジャーナル(1本)に採択された．また，ハイブリッド符号化とその関連研究について，研究分担者が第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)の発表賞(一般の部)を受賞した．
(D)について，時間割編成とシステム生物学に関する応用研究を行った．これらの成果は，国際ジャーナル(2本)と国際会議(3本)に採択された．さらに，回路の配線問題と親和性の高い多層ナンバーリンクを解く ASP プログラムを開発し，アルゴリズムデザインコンテスト(DAシンポジウム2016に併設)において第2位となり優秀賞を受賞した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究は交付申請書に記載した「研究実施計画」に照らして順調に進捗している．
最終年度である平成29年度に計画されている(C)の制約 ASP ソルバーの拡張，(D)の制約 ASP の特長的なアプリケーションの開発および問題記述例の蓄積について，その準備状況を述べる．
近年人工知能分野を中心に多目的最適化問題に関する研究開発が活発化している．多目的最適化問題の解は，パレート最適性によって定義され，実問題のもつトレードオフ関係にある多様な解を表現できる．我々は SAT 符号化と極小モデル生成を用いた多目的最適化問題の解法について研究開発を進めており，最近得られた成果を国際会議に投稿中である．(C)については，この研究成果を用いて制約 ASP ソルバーを拡張することで，効率の良い多目的最適化が実現できることが期待できる．
(D)について，複数の評価基準をもつテストケース生成問題の解法について研究開発を進めている．この成果の一部をまとめた論文は，国際会議 LPNMR2017 に採録が決定している．このソフトウェアのテストケース生成については，近年ソフトウェア工学分野を中心に多くの研究開発が進めれている．制約 ASP のソフトウェア工学への応用という観点からも，特長的なアプリケーションとして期待できる．この他にも，特長的なアプリケーションとして，部分グラフ探索，ペトリネットのデッドロック検出などについて研究調査を開始している．
|
| Strategy for Future Research Activity |
最終年度である平成29年度は，(C)の制約 ASP ソルバー拡張，(D)のアプリケーション開発および問題記述例の蓄積を完了する．そして最後に，(D)の問題群を用いて，(B)と(C)で開発したソルバーの総合的な評価を行う．
これまでに，(A)の制約 ASP 言語に関する研究，(B)の制約 ASP ソルバー開発を完了している．(B)では2種類の制約 ASP ソルバー Aspartame と clingconを設計・実装した．Aspartame は SAT 符号化に基づく符号化型ソルバーであり，clingcon は背景論理に基づく SMT 型ソルバーである．本研究の総合的な評価を行う際には，これら2種類のソルバーの長所・短所を詳しく研究調査し明らかにすることが重要である．
(C)では，ハイブリッド符号化，インクリメンタル解法の研究成果，および現在進めている多目的最適化の研究を元に，(B)で開発した2種類の制約 ASP ソルバーを拡張する．これにより，より大規模な制約充足問題および(多目的)制約最適化問題を効率よく求解できるようになることが期待できる．(D)のアプリケーションについては，時間割問題，システム生物学の諸問題，テストケース生成問題，回路の配線問題を中心に研究を進める．
研究代表者・番原と連携研究者・井上の研究拠点が離れているため，4名の研究者全員が参加する研究打合せを年2回開催する．ここでは，アイデア・実現技術の共有を主目的とし，進捗状況の報告，研究計画・方法に関する議論を行う.海外共同研究者はこの研究打合せに年1回参加し，本研究に関連する海外での最新動向の紹介などを通して本研究の推進に寄与する. このような密接な協力体制を整えることによって，研究が当初の計画通りに進まない場合，研究者間で対応策を検討し，研究計画・方法の見直し等を速やかに行えると考えている．
|
Research Products
(24 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] SAT ソルバーの進歩2017
Author(s)
番原睦則
Organizer
2017年電子情報通信学会総合大会
Place of Presentation
名城大学 (愛知県・名古屋市)
Year and Date
2017-03-22 – 2017-03-25
Invited
-
-
-
-
-
-
-
-
-
-
-
