首页> 外文会议>International Conference on Artificial Intelligence Planning and Scheduling; 2000414-17; Breckenridge,CO(US) >Investigating the Effect of Relevance and Reachability Constraints on SAT Encodings of Planning
【24h】

Investigating the Effect of Relevance and Reachability Constraints on SAT Encodings of Planning

机译:研究相关性和可达性约束对计划的SAT编码的影响

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

摘要

Currently, Graphplan and Blackbox, which converts Graph-plan's plan graph into the satisfaction (SAT) problem, are two of the most successful planners. Since Graphplan gains its efficiency from the forward propagation of reachability based mutual exclusion constraints (mutex) and their backward use, it has been believed that SAT encoding will also benefit from mutexes. In this paper, we will try to answer two important questions: (1) Are mutual exclusions actually useful for solution extraction in SAT encoding? (2) Are there other useful constraints that can be propagated on the planning graph which may help SAT solvers ? Our experiments with systematic solvers Relsat and Satz shows that though forward mutexes are useful in general, there are domains in which mutex constraints can slow down search. Moreover, we introduce the notion of backward mutex and their propagation which is based on relevance analysis and implement it in Blackbox. We find that the addition of relevance based backward mutual exclusions helps speedup the Relsat solver in solving the SAT encoding of many standard planning problems.
机译:当前,将Graph-plan的计划图转换为满意度(SAT)问题的Graphplan和Blackbox是最成功的两个计划者。由于Graphplan通过基于可达性的互斥约束(mutex)的前向传播及其反向使用而获得了效率,因此人们认为SAT编码也将从互斥锁中受益。在本文中,我们将尝试回答两个重要的问题:(1)互斥实​​际上对SAT编码中的解提取有用吗? (2)在规划图上是否还可以传播其他有用的约束,这些约束可以帮助SAT求解器?我们使用系统求解器Relsat和Satz进行的实验表明,尽管前向互斥锁通常很有用,但在某些域中,互斥锁约束可能会减慢搜索速度。此外,我们介绍了基于相关性分析的后向互斥及其传播概念,并在Blackbox中实现。我们发现,基于相关性的向后互斥性的添加有助于加快Relsat求解器解决许多标准计划问题的SAT编码的速度。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号