Unsolvability Certificates for Classical Planning
Unsolvability Certificates for Classical Planning
复制标题
经典规划的不可解性证明
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
M. Helmert
中科院分区：
文献类型：
--
作者：
Salomé Eriksson;Gabriele Röger;M. Helmert
规划系统为可解决的规划任务生成的计划通常由独立的验证工具进行验证。对于无法解决的计划任务，目前不存在此类验证功能。我们描述了一个家庭的经典规划任务，可以有效地验证，并足够广泛的规划方法，包括启发式搜索删除松弛，关键路径，模式数据库和线性合并和收缩算法，符号搜索与二进制决策图，和陷阱算法检测死胡同的不可解性证书。我们还增加了一个经典的规划系统，能够发出证书的不可解性，并实现了一个计划独立的证书验证工具。实验表明，产生这种证书的开销是可以容忍的，他们的验证是实际可行的。
The plans that planning systems generate for solvable planning tasks are routinely verified by independent validation tools. For unsolvable planning tasks, no such validation capabilities currently exist. We describe a family of certificates of unsolvability for classical planning tasks that can be efficiently verified and are sufficiently general for a wide range of planning approaches including heuristic search with delete relaxation, critical-path, pattern database and linear merge-and-shrink heuristics, symbolic search with binary decision diagrams, and the Trapper algorithm for detecting dead ends. We also augmented a classical planning system with the ability to emit certificates of unsolvability and implemented a planner-independent certificate validation tool. Experiments show that the overhead for producing such certificates is tolerable and that their validation is practically feasible.