効率的なSATプランニングとSATスケジューリングのための補題再利用 Effective SAT Planning and SAT Scheduling by Lemma Reusing

この論文をさがす

著者

抄録

本稿では,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.

収録刊行物

  • 電子情報通信学会技術研究報告. AI, 人工知能と知識処理

    電子情報通信学会技術研究報告. AI, 人工知能と知識処理 106(38), 19-24, 2006-05-11

    一般社団法人電子情報通信学会

参考文献:  17件中 1-17件 を表示

各種コード

  • NII論文ID(NAID)
    110004744913
  • NII書誌ID(NCID)
    AN10013061
  • 本文言語コード
    ENG
  • 資料種別
    ART
  • ISSN
    09135685
  • NDL 記事登録ID
    7937821
  • NDL 雑誌分類
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL 請求記号
    Z16-940
  • データ提供元
    CJP書誌  NDL  NII-ELS 
ページトップへ