首页> 外文会议>International Conference on Automated Planning and Scheduling(ICAPS 2006); 2006; >Friends or Foes? An AI Planning Perspective on Abstraction and Search
【24h】

Friends or Foes? An AI Planning Perspective on Abstraction and Search

机译:朋友还是敌人?关于抽象和搜索的AI规划观点

获取原文
获取原文并翻译 | 示例

摘要

There is increasing awareness that planning and model checking are closely related fields. Abstraction means to perform search in an over-approximation of the original problem instance, with a potentially much smaller state space. This is the most essential method in model checking. One would expect that it can also be made successful in planning. We show, however, that this is likely to not be the case. The main reason is that, while in model checking one traditionally uses blind search to exhaust the state space and prove the absence of solutions, in planning informed search is used to find solutions. We give an exhaustive theoretical and practical account of the use of abstraction in planning. For all abstraction (over-approximation) methods known in planning, we prove that they cannot improve the best-case behavior of informed search. While this is easy to see for heuristic search, we were quite surprised to find that it also holds, in most cases, for the resolution-style proofs of unsolvability underlying SAT-based optimal planners. This result is potentially relevant also for model checking, where SAT-based techniques have recently been combined with abstraction. Exploring the issue in planning practice, we find that even hand-made abstractions do not tend to improve the performance of planners, unless the attacked task contains huge amounts of irrelevance. We relate these findings to the kinds of application domains that are typically addressed in model checking.
机译:人们越来越意识到规划和模型检查是紧密相关的领域。抽象意味着在原始问题实例的近似值中执行搜索,并且状态空间可能要小得多。这是模型检查中最重要的方法。人们希望它也可以成功地进行规划。但是,我们证明情况可能并非如此。主要原因是,尽管在模型检查中传统上使用盲搜索来耗尽状态空间并证明不存在解决方案,但在计划中使用知情搜索来找到解决方案。我们对规划中使用抽象进行了详尽的理论和实践说明。对于计划中已知的所有抽象(过度逼近)方法,我们证明它们不能改善知情搜索的最佳情况。尽管对于启发式搜索而言这很容易看到,但令我们惊讶的是,它在大多数情况下也适用于基于SAT的最佳规划者不可解决的分辨率式证明。该结果也可能与模型检查相关,因为最近基于SAT的技术已与抽象技术结合在一起。在计划实践中探讨该问题时,我们发现,即使手工制作的抽象也无法提高计划者的性能,除非被攻击的任务包含大量无关紧要的内容。我们将这些发现与模型检查中通常解决的应用程序领域相关。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号