SATプランニングとスケジューリングの高度化・高速化に関する研究

• 研究課題/領域番号: 19700135
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: 知能情報学
• 研究機関: 山梨大学
• 研究代表者: 鍋島 英知 山梨大学, 大学院・医学工学総合研究部, 准教授 (10334848)
• 研究期間 (年度): 2007 – 2009
• 研究課題ステータス: 完了 (2009年度)
• 配分額: 3,810千円 (直接経費: 3,300千円、間接経費: 510千円); 2009年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円); 2008年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2007年度: 1,600千円 (直接経費: 1,600千円)
• キーワード: 充足可能性問題 / プランニング / スケジューリング / 分散協調

研究概要

命題論理の充足可能性問題(satisfiability problem ; SAT問題)を利用したSATプランニングやSATスケジューリングなどの問題解決手法では,一般に複数のSAT問題を解く必要がある.これら複数のSAT問題を効率良く解くために,我々は,探索過程で得られる補題・仮説・モデルを再利用するPCクラスタ向け分散協調SATソルバSatCubeを開発した.また,SATプランニングの適用範囲拡大のため順序符号化法に基づく拡張の検討と,SATスケジューリングに対する各種の高速化技術を開発した.

研究成果

• [雑誌論文] 高速SATソルバーの原理 (2010)
  • 著者名/発表者名: 鍋島英知, 宋剛秀
  • 雑誌名: 人工知能学会誌 Vol.25,No.1 ページ: 68-76
• [雑誌論文] SMT:個別理論を取り扱うSAT技術 (2010)
  • 著者名/発表者名: 岩沼宏治, 鍋島英知
  • 雑誌名: 人工知能学会誌 Vol.25,No.1 ページ: 86-95
• [雑誌論文] SATによるプランニングとスケジューリング (2010)
  • 著者名/発表者名: 鍋島英知
  • 雑誌名: 人工知能学会誌 Vol.25,No.1 ページ: 114-121
• [雑誌論文] SOLAR: An Automated Deduction System for Consequence Finding (2010)
  • 著者名/発表者名: Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue, Oliver Ray
  • 雑誌名: AI Communications Vol.23,No.2-3 ページ: 183-203
  • 査読あり
• [雑誌論文] SOLAR : An Automated Deduction System for Consequence Finding (2010)
  • 著者名/発表者名: Hidetomo Nabeshima
  • 雑誌名: AI Communications 23, 2-3 ページ: 183-203
  • 査読あり
• [雑誌論文] 高速SATソルバの原理 (2010)
  • 著者名/発表者名: 鍋島英知
  • 雑誌名: 人工知能学会誌 25, 1 ページ: 68-76
• [雑誌論文] SMT:個別理論を取り扱うSAT技術 (2010)
  • 著者名/発表者名: 岩沼宏治
  • 雑誌名: 人工知能学会誌 25, 1 ページ: 86-95
• [雑誌論文] SATによるプランニングとスケジューリング (2010)
  • 著者名/発表者名: 鍋島英知
  • 雑誌名: 人工知能学会誌 25, 1 ページ: 114-121
• [雑誌論文] Evaluating Abductive Hypotheses using an EM Algorithm on BDDs. (2009)
  • 著者名/発表者名: Katsumi Inoue, Taisuke Sato, Masakazu Ishihata, Yoshitaka Kameya, Hidetomo Nabeshima
  • 雑誌名: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI-09) ページ: 810-815
  • 査読あり
• [雑誌論文] Minimal Model Generation with Respect to an Atom Set (2009)
  • 著者名/発表者名: Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, Ryuzo Hasegawa
  • 雑誌名: Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP 2009) ページ: 49-59
  • 査読あり
• [雑誌論文] Evaluating Abductive Hypotheses using an EM Algorithm on BDDs (2009)
  • 著者名/発表者名: Katsumi Inoue
  • 雑誌名: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI-09) ページ: 810-815
  • 査読あり
• [雑誌論文] Minimal Model Generation with Respect to an Atom Set (2009)
  • 著者名/発表者名: Miyuki Koshimura
  • 雑誌名: Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP 2009) ページ: 49-59
  • 査読あり
• [雑誌論文] A SAT-based Method for Solving the Two-dimensional Strip Packing Problem. Proceedings of the 15th International RCRA workshop (RCRA 2008) (2008)
  • 著者名/発表者名: Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
  • 雑誌名: Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion Vol.451 ページ: 25-39
  • 査読あり
• [雑誌論文] A Complete Pruning Methods and a Practical Search Strategy for SOL, Proceedings of the LPAR 2008 Workshops on Knowledge Exchange (2008)
  • 著者名/発表者名: Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue
  • 雑誌名: Automated Provers and Proof Assistants and The 7th International Workshop on the Implementation of Logics (IWIL 2008) Vol.418 ページ: 113-122
  • 査読あり
• [雑誌論文] A SAT-based Method for Solving the Two-dimensional Strip Packing Problem (2008)
  • 著者名/発表者名: Takehide Soh
  • 雑誌名: 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion ページ: 25-39
  • 査読あり
• [雑誌論文] A Complete Pruning Methods and a Practical Search Strategy for SOL (2008)
  • 著者名/発表者名: Hidetomo Nabeshima
  • 雑誌名: 7th International Workshop on the Implementation of Logics (IWIL 2008) 418 ページ: 113-122
  • 査読あり
• [学会発表] SAT変換による未解決ジョブショップ・スケジューリング問題への挑戦 (2009)
  • 著者名/発表者名: 越村三幸, 鍋島英知, 藤田博, 長谷川隆三
  • 学会等名: スケジューリング・シンポジウム2009講演論文集
  • 発表場所: 岡山大学
  • 年月日: 2009-09-17
• [学会発表] SAT変換による未解決ジョブショップ・スケジューリング問題への挑戦 (2009)
  • 著者名/発表者名: 越村三幸
  • 学会等名: スケジューリング・シンポジウム2009
  • 発表場所: 岡山大学
  • 年月日: 2009-09-17
• [学会発表] 並列分散型SATソルバにおける探索空間の分割手法の提案 (2009)
  • 著者名/発表者名: 高見明秀, 鍋島英知, 岩沼宏治
  • 学会等名: 電子情報通信学会技術研究報告IEICE-SS-444
  • 発表場所: 佐賀大学
  • 年月日: 2009-03-02
• [学会発表] マルチコア環境に向けた高速並列SATソルバの開発 (2007)
  • 著者名/発表者名: 高見明秀, 鍋島英知, 岩沼宏治
  • 学会等名: 第6回情報科学技術フォーラム
  • 発表場所: 中京大学
  • 年月日: 2007-09-07
• [学会発表] マルチコア環境向け並列SATソルバの開発 (2007)
  • 著者名/発表者名: 高見明秀, 鍋島英知, 岩沼宏治
  • 学会等名: 電子情報通信学会技術研究報告
  • 発表場所: 機会振興会館
  • 年月日: 2007-05-24
• [学会発表] マルチコア環境に向けた高速並列SATソルバの開発 (2007)
  • 著者名/発表者名: 高見 明秀
  • 学会等名: 電子情報通信学会技術研究報告 AI2007-2
  • 発表場所: 機会振興会館
  • 年月日: 2007-05-24
• [図書] ナノオプトニクスエナジー(ロボット情報学ハンドブック) (2010)
  • 著者名/発表者名: 松原仁, 他