| 講演名 | 2006-05-18 効率的なSATプランニングとSATスケジューリングのための補題再利用(「自動化:推論,発見,学習,データマイニング」及び一般) 鍋島 英知, 宋 剛秀, 井上 克巳, 岩沼 宏治, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では,SATプランニングとSATスケジューリングを効率よく解くために補題再利用手法を提案し,その効果を実証する.一般的に,SATプランニングやSATスケジューリングなどのSAT符号化手法においては,徐々に大きくなるSAT問題の列を解く必要がある.多くの最新のSATソルバは,冗長な探索空間を狩り取るために補題を学習し利用している.しかし,あるSAT問題から生成された補題は,基本的に他のSAT問題を解くために利用することはできない.本稿では,SATプランニングとSATスケジューリングにおけるある特定のSAT符号化においては補題が再利用可能であることを証明し,補題を再利用することにより効率的に問題を解くことができることを実証する. |
| 抄録(英) | In this paper, we propose a new approach, called lemma-reusing, for accelerating SAT based planning and scheduling. Generally, SAT based approaches generate a sequence of SAT problems which become larger and larger. A SAT solver needs to solve the problems until it encounters a satisfiable SAT problem. Many state-of-the-art SAT solvers learn lemmas called conflict clauses to prune redundant search space, but lemmas deduced from a certain SAT problem can not apply to solve other SAT problems. However, in certain SAT encodings of planning and scheduling, we prove that lemmas generated from a SAT problem are reusable for solving larger SAT problems. We implemented the lemma-reusing planner (LRP) and the lemma-reusing job shop scheduling problem solver (LRS). The experimental results show that LRP and LRS are faster than lemma-no-reusing ones. |
| キーワード(和) | 充足可能性問題 / プランニング / スケジューリング |
| キーワード(英) | SAT / planning / scheduling |
| 資料番号 | AI2006-4 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2006/5/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | 効率的なSATプランニングとSATスケジューリングのための補題再利用(「自動化:推論,発見,学習,データマイニング」及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Effective SAT Planning and SAT Scheduling by Lemma Reusing |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 充足可能性問題 / SAT |
| キーワード(2)（和/英） | プランニング / planning |
| キーワード(3)（和/英） | スケジューリング / scheduling |
| 第 1 著者 氏名（和/英） | 鍋島 英知 / Hidetomo NABESHIMA |
| 第 1 著者 所属（和/英） | 山梨大学 大学院 医学工学総合研究部 Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi |
| 第 2 著者 氏名（和/英） | 宋 剛秀 / Takehide SOH |
| 第 2 著者 所属（和/英） | 神戸大学 大学院 自然科学研究科 Graduate School of Science and Technology, Kobe University |
| 第 3 著者 氏名（和/英） | 井上 克巳 / Katsumi INOUE |
| 第 3 著者 所属（和/英） | 国立情報学研究所 National Institute of Informatics |
| 第 4 著者 氏名（和/英） | 岩沼 宏治 / Koji IWANUMA |
| 第 4 著者 所属（和/英） | 山梨大学 大学院 医学工学総合研究部 Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi |
| 発表年月日 | 2006-05-18 |
| 資料番号 | AI2006-4 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 38 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |