2020 Fiscal Year Annual Research Report
Engineering Approach for Expanding Combinatorial Reconfiguration: Toward a General-Purpose Solver Using Power Distribution Systems as a Steppingstone
| Project Area | Fusion of Computer Science, Engineering and Mathematics Approaches for Expanding Combinatorial Reconfiguration |
|---|
| Project/Area Number |
20H05794
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
川原 純 京都大学, 情報学研究科, 准教授 (20572473)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
飯岡 大輔 中部大学, 工学部, 准教授 (30377808)
戸田 貴久 電気通信大学, 大学院情報理工学研究科, 准教授 (50451159)
宋 剛秀 神戸大学, 情報基盤センター, 准教授 (00625121)
鈴木 顕 東北大学, 情報科学研究科, 准教授 (10723562)
照山 順一 兵庫県立大学, 社会情報科学部, 助教 (40709862)
|
|---|
| Project Period (FY) |
2020-10-02 – 2023-03-31
|
| Keywords | 組合せ遷移 / グラフアルゴリズム / SAT / モデル検査 / ゼロサプレス型二分決定グラフ |
|---|
| Outline of Annual Research Achievements |
本研究では組合せ遷移の実装技術の構築とその産業応用に向けて、研究開発の共通基盤となるソフトウェア開発を目標とする。初年度にあたる本年度は、広く知られているグラフの独立集合の遷移問題（独立集合遷移問題）に対して、4種のアプローチを検討した。1つ目は、組合せ遷移の技法を用いたアルゴリズムの設計であり、主に、状態空間の部分探索の手法を検討した。2つ目は、SAT（充足可能性問題）ソルバーを活用するアプローチである。有限整数領域上の制約を命題論理式へと変換する SAT 符号化を行い、SATソルバーの強力な推論性能を用いて独立集合遷移問題を解くソルバーを開発した。3つ目は、ゼロサプレス型二分決定グラフ (ZDD) を活用するアプローチである。当初予定では、ZDD を上記2手法に援用した高速化を想定していたが、本研究において、ZDD が表す独立集合族を直接遷移させるアルゴリズムの開発に成功したため、ZDD を単独で用いて独立集合遷移問題を解くことが可能になった。4つ目の手法は、当初は予定していない新たな構想であるが、モデル検査と呼ばれる、システムの形式的な検査を可能にする技術を用いた手法である。入力グラフと開始、目標独立集合が与えられた際に、開始集合から目標集合に遷移可能ではないことを検証する記述をモデル検査ソルバーに与え、遷移可能な場合は反例として解となる遷移列を出力する。
以上の4つの技法について、アルゴリズム設計と実装を行った。アルゴリズムの比較実験のためには、適切な入力データが必要であるが、組合せ遷移問題に対する広く知られたベンチマークデータは存在しないため、入力データの作成整備を行った。
配電切替への組合せ遷移技術の適用についても研究を行い、配電切替を全域木遷移問題として定式化し、4つの技法の適用を検討して、実装を行っている。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初に予定していた独立集合遷移問題に対する3つの技法の開発状況としては、アルゴリズム設計と実装が完了し、さらに当初に予定していなかったモデル検査を用いた技法についてもアルゴリズム設計と実装が完了している。配電切替への組合せ遷移技術の適用についても、当初の予定通りに進んでいる。おおむね順調に進展していると言える。
|
| Strategy for Future Research Activity |
来年度は独立集合遷移問題に対する4つの技法について、高速化や汎用化などの方向で発展させる。独立集合遷移問題だけでなく、全域木遷移問題やマッチング遷移問題など、様々な組合せ遷移問題に適用可能な汎用的な技法の開発を行う。特に、SATやモデル検査については、符号化手法を問題に応じて変更することで、様々な組合せ遷移問題に対応できると考えられるため、どの程度符号化に汎用性があるのか見極めを行い、アルゴリズムの専門家ではない組合せ遷移問題を解きたい利用者でも符号化が可能になるように、技法の整備を行う。ZDDを用いた技法については、従来研究において、入力グラフの全域木集合やマッチングの集合、弦グラフの集合など、様々な部分グラフの集合をZDDとして圧縮状態で保持する手法が提案されており、それらの手法を用いることで組合せ遷移問題への適用が可能であると見込まれ、研究を行う。
4つの技法について、比較実験を行い、入力データに応じた各技法の特性を調査する。4つの技法は、どれか1つがすべての面において優れていることは考えにくく、入力データに対する得手不得手が存在すると考えられ、それらを見極める。また、独立集合遷移問題だけでなく、他の組合せ遷移問題に対しても比較を行う。
配電切替への組合せ遷移技術の適用についても引き続き4つの技法の適用を検討する。
独立集合遷移問題やその他の遷移問題を一般の利用者が解くことが可能なGUI（ユーザインターフェース）付きソフトウェア開発も行う。
|
