• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Logical Methods in Computer Science >Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning
【24h】

Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning

机译：结构和问题难度：基于SAT的规划中的目标不对称性和DPLL证明

获取原文
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In Verification and in (optimal) AI Planning, a successful method is toformulate the application as boolean satisfiability (SAT), and solve it withstate-of-the-art DPLL-based procedures. There is a lack of understanding of whythis works so well. Focussing on the Planning context, we identify a form ofproblem structure concerned with the symmetrical or asymmetrical nature of thecost of achieving the individual planning goals. We quantify this sort ofstructure with a simple numeric parameter called AsymRatio, ranging between 0and 1. We run experiments in 10 benchmark domains from the InternationalPlanning Competitions since 2000; we show that AsymRatio is a good indicator ofSAT solver performance in 8 of these domains. We then examine carefully craftedsynthetic planning domains that allow control of the amount of structure, andthat are clean enough for a rigorous analysis of the combinatorial searchspace. The domains are parameterized by size, and by the amount of structure.The CNFs we examine are unsatisfiable, encoding one planning step less than thelength of the optimal plan. We prove upper and lower bounds on the size of thebest possible DPLL refutations, under different settings of the amount ofstructure, as a function of size. We also identify the best possible sets ofbranching variables (backdoors). With minimum AsymRatio, we prove exponentiallower bounds, and identify minimal backdoors of size linear in the number ofvariables. With maximum AsymRatio, we identify logarithmic DPLL refutations(and backdoors), showing a doubly exponential gap between the two structuralextreme cases. The reasons for this behavior -- the proof arguments --illuminate the prototypical patterns of structure causing the empiricalbehavior observed in the competition benchmarks.
机译：在验证和（最佳）AI计划中，一种成功的方法是将应用程序构造为布尔可满足性（SAT），并使用基于DPLL的最新过程对其进行求解。缺乏对为什么如此有效的理解。着眼于计划环境，我们确定了一种形式的问题结构，涉及实现单个计划目标的成本的对称性或非对称性。我们使用名为AsymRatio的简单数值参数（介于0和1之间）对这种结构进行量化。自2000年以来，我们在国际规划竞赛的10个基准域中进行了实验;我们显示，AsymRatio是这8个域中SAT求解器性能的良好指标。然后，我们检查精心设计的合成规划域，这些域可以控制结构的数量，并且足够干净，可以对组合搜索空间进行严格的分析。通过大小和结构数量来对域进行参数化。我们研究的CNF不能令人满意，其编码步骤比最佳计划的长度短。我们证明了在不同数量的结构设置下，最大可能的DPLL反驳的大小的上限和下限。我们还将确定分支变量（后门）的最佳可能集合。利用最小的AsymRatio，我们证明了指数下界，并确定了变量数量线性最小的后门。借助最大的AsymRatio，我们确定了对数DPLL反驳（和后门），显示了两种结构极端情况之间的双指数差距。这种行为的原因-证明论点-阐明了导致竞争基准中观察到的经验行为的结构原型模式。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号