SATソルバを用いた高速プランニングのための統合的システムに関する研究

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12680384
• Research Institution: Kobe University
• Principal Investigator: 井上 克巳 神戸大学, 工学部, 助教授 (10252321)
• Co-Investigator(Kenkyū-buntansha): 鍋島 英知 山梨大学, 工学部, 助手 (10334848) ; 羽根田 博正 神戸大学, 工学部, 教授 (10031113)
• Keywords: プランニング / 状態変化 / 推論 / 充足可能性問題 / アクション言語 / SATプランニング / プランニンググラフ / SATソルバ

Research Abstract

SATプランニングは,プランニング(計画作成)問題を充足可能性判定問題(SAT)に変換し,高速SATソルバによりモデルを生成しプランに変換する手法である.本研究では,知識表現の研究分野で開発されてきたアクション言語を入力として,高速なSATプランニングを行うことができる,統合的なアクション言語処理系を構築することを研究の目的としている.
研究期間は2年であり,2年目に当たる平成13年度は,1年目に検討した研究成果を基に統合的プランニングシステムAMPを開発整備した.具体的には以下の3点に分けて研究を進めた.
1.アクション言語処理系のためのアルゴリズムの検討
プランニンググラフをデータ構造として用いて,前向き/後向き/双方向の3種のグラフ展開アルゴリズムを発展させ,無駄な探索をせずにプラン抽出ができるように工夫した.さらに,非決定性アクションを含むプランニング問題を、どのようにしてSAT問題に変換するか考察した.
2.学習アルゴリズムの検討
アクションの因果関係を学習するアルゴリズムを引続き検討し,これを用いてさらなるプランニングの高速化を図った.
3.システムの実装および評価
これまでに開発したプランニング・アルゴリズムを基に実装を行った.プランナのベースとなるSATソルバも交換可能な設計とし,複数のエンジンを問題に応じて選択できるようにした.また,プランニングシステムの性能を評価するために,ベンチマーク問題を利用した現実的な問題に対する有用性を図るために,規模の大きなプランニング問題について実験し検証した.
以上のように,本研究により開発した統合的システムAMPは,状態変化やアクションを表現する研究とプランニング研究の双方にとって.非常に有用なものであるといえる.

Research Products

• [Publications] 鍋島 英知: "プランニンググラフとSATプランニング"人工知能学会誌. 16・5. 605-610 (2001)
• [Publications] Katsumi Inoue: "Induction, Abduction, and Consequence-Finding"Lecture Notes in Artificial Intelligence. 2157. 65-79 (2001)
• [Publications] Katsumi Inoue: "Automated Abduction"Lecture Notes in Artificial Intelligence. (to appear). (2002)