结构与问题难度：基于 SAT 的规划中的目标非对称性与 DPLL 证明
人工智能
2017-01-11 v2
摘要
在验证与（最优）AI 规划中，一种成功的方法是将应用表述为布尔可满足性 (SAT)，并用最先进的基于 DPLL 的过程来求解。目前缺乏对为何此方法如此有效的理解。聚焦于规划背景，我们识别了一种与实现各个规划目标的代价对称或非对称性质相关的问题结构形式。我们用一个称为 AsymRatio 的简单数值参数来量化这种结构，其取值范围在 0 到 1 之间。我们在自 2000 年以来国际规划竞赛的 10 个基准领域中进行了实验；结果表明，AsymRatio 是其中 8 个领域中 SAT 求解器性能的良好指标。随后，我们仔细检查了经过精心设计的合成规划领域，这些领域允许控制结构的数量，并且足够清晰以便对组合搜索空间进行严格分析。这些领域由规模和结构数量进行参数化。我们检查的 CNF 是不可满足的，编码了比最优规划长度少一步的规划。作为规模的函数，我们证明了在不同结构数量设置下最佳可能 DPLL 反演大小的上界和下界。我们还识别了最佳可能的分支变量集（后门）。在 AsymRatio 最小的情况下，我们证明了指数下界，并识别出大小与变量数成线性关系的最小后门。在 AsymRatio 最大的情况下，我们识别出对数级的 DPLL 反演（和后门），表明这两个结构极端情况之间存在双指数差距。这种行为的原因——即证明论证——阐明了导致在竞赛基准中观察到的经验行为的典型结构模式。
引用
@article{arxiv.cs/0701184,
title = {Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in<br> SAT-Based Planning},
author = {Joerg Hoffmann and Carla Gomes and Bart Selman},
journal= {arXiv preprint arXiv:cs/0701184},
year = {2017}
}