講演名 2003/5/22
補題再利用によるSATプランニングの高速化(<特集>「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(自動推論)
鍋島 英知, 野沢 宏仁, 岩沼 宏治,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 本橋では,SATプランニングの効率を改善するために,補題を再利用する手法を提案する.一般的に,あるSAT問題から生成された補題は別のSAT問題において利用することはできない.しかし我々は,世界最遠のSATソルバの1つであるChaffが生成する補題に関しては,SATプランニングにおいて生成された複数のSAT問題において,補題が再利用可能であることを示す.我々は,補題を再利用するSATプランニングアルゴリズムLRPを提案し,その正当性を証明する.評価実験の結果,LRPが補題を再利用しない場合と比較して,約160%高速であることが示された.
抄録(英) In this paper, we propose a new approach for improving efficiency of SAT planning by lemma-reusing. Generally, a lemma derived from a SAT problem can not apply to other SAT problems. However, we prove that lemmas generated by Chaff which is the fastest SAT solver in the world are applicable to other SAT problems generated in SAT planning. We propose a new SAT planning approach LRP which reuses such lemmas, and prove the correctness. The experimental results show that LRP is 160% faster than Blackbox that does not reuse lemmas.
キーワード(和) SATプランニング / 充足可能性問題 / 補題
キーワード(英) SAT planning / Satisfiablitiy / Lemma
資料番号 AI2003-9
発行日

研究会情報
研究会 AI
開催期間 2003/5/22(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Artificial Intelligence and Knowledge-Based Processing (AI)
本文の言語 JPN
タイトル(和) 補題再利用によるSATプランニングの高速化(<特集>「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(自動推論)
サブタイトル(和)
タイトル(英) Effective SAT Planning by Lemma-Reusing
サブタイトル(和)
キーワード(1)(和/英) SATプランニング / SAT planning
キーワード(2)(和/英) 充足可能性問題 / Satisfiablitiy
キーワード(3)(和/英) 補題 / Lemma
第 1 著者 氏名(和/英) 鍋島 英知 / Hidetomo NABESHIMA
第 1 著者 所属(和/英) 山梨大学大学院医学工学統合研究部
Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi
第 2 著者 氏名(和/英) 野沢 宏仁 / Hirohito NOZAWA
第 2 著者 所属(和/英) 株式会社アム
AM Corporation,
第 3 著者 氏名(和/英) 岩沼 宏治 / Koji IWANUMA
第 3 著者 所属(和/英) 山梨大学大学院医学工学統合研究部
Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi
発表年月日 2003/5/22
資料番号 AI2003-9
巻番号(vol) vol.103
号番号(no) 103
ページ範囲 pp.-
ページ数 6
発行日