• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Automated Planning and Scheduling(ICAPS 2006); 2006; >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 AI Planning, as well as Verification, a successful method is to compile the application into boolean satisfiability (SAT), and solve it with state-of-the-art DPLL-based procedures. There is a lack of formal understanding why this works so well. Focussing on the Planning context, we identify a form of problem structure concerned with the symmetrical or asymmetrical nature of the cost of achieving the individual planning goals. We quantify this sort of structure with a simple numeric parameter called AsymRatio, ranging between 0 and 1. We show empirically that AsymRatio correlates strongly with SAT solver performance in a broad range of Planning benchmarks, including the domains used in the 3rd International Planning Competition. We then examine carefully crafted synthetic planning domains that allow to control the amount of structure, and that are clean enough for a rigorous analysis of the combinatorial search space. The domains are parameterized by size n, and by a structure parameter fc, so that AsymRatio is asymptotic to k. The CNFs we examine are unsatisfiable, encoding one planning step less than the length of the optimal plan. We prove upper and lower bounds on the size of the best possible DPLL refutations, under different settings of fc, as a function of n. We also identify the best possible sets of branching variables (backdoors). With minimum AsymRatio, we prove exponential lower bounds, and identify minimal backdoors of size linear in the number of variables. With maximum AsymRatio, we identify logarithmic DPLL refutations (and backdoors), showing a doubly exponential gap between the two structural extreme cases. This provides a concrete insight into the practical efficiency of modern SAT solvers.
机译：在AI Planning和Verification中，一种成功的方法是将应用程序编译为布尔可满足性（SAT），并使用基于DPLL的最新过程对其进行求解。缺乏形式上的解释为什么如此有效。着眼于计划上下文，我们确定一种与实现单个计划目标的成本的对称或不对称性质有关的问题结构。我们使用一个称为AsymRatio的简单数值参数（介于0和1之间）对这种结构进行量化。我们在广泛的Planning基准测试中（包括在第三届国际计划竞赛中使用的域），通过实验证明了AsymRatio与SAT求解器的性能密切相关。然后，我们检查精心设计的综合规划领域，这些领域可以控制结构量，并且足够干净，可以对组合搜索空间进行严格的分析。通过大小n和结构参数fc对域进行参数化，以使AsymRatio渐近于k / n。我们检查的CNF不能令人满意，其编码步骤少于最佳计划的长度。我们证明了在fc的不同设置下，最佳的DPLL反驳的大小的上下限是n的函数。我们还确定了最佳的分支变量集（后门）。使用最小的AsymRatio，我们证明了指数下界，并确定了变量数量中线性最小的后门。利用最大的AsymRatio，我们确定了对数DPLL反驳（和后门），显示出两种结构极端情况之间的双指数差距。这为现代SAT解算器的实际效率提供了具体见解。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号