SAS+ Planning as Satisfiability
SAS+ Planning as Satisfiability
复制标题
SAS 规划作为可满足性
DOI：
10.1613/jair.3442
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Weixiong Zhang
中科院分区：
文献类型：
--
作者：
Ruoyun Huang;Yixin Chen;Weixiong Zhang
作为可满足性的规划是规划的一种主要方法，具有许多突出的优点。现有的规划作为可满足性技术，通常使用编译自可满足性规划的编码。我们介绍了一种新的SAT编码方案（SASE）的基础上的SAS+形式主义。新方案利用了SAS+中的结构信息，从而产生了一种更紧凑、更有效的编码。我们证明了新的编码的正确性，通过建立一个同构的解决方案之间的计划SASE和基于编码的SAMPS。我们进一步分析了SASE中新引入的过渡变量，以解释为什么它可以容纳现代SAT求解算法并提高性能。我们给出了实证统计结果来支持我们的分析。我们还开发了一些技术，以进一步减少SASE的编码大小，并进行实验研究，以显示每个单独的技术的强度。最后，我们报告了大量的实验结果，以证明显着的改进SASE在国家的最先进的基于编码方案的时间和内存效率。
Planning as satisfiability is a principal approach to planning with many eminent advantages. The existing planning as satisfiability techniques usually use encodings compiled from STRIPS. We introduce a novel SAT encoding scheme (SASE) based on the SAS+ formalism. The new scheme exploits the structural information in SAS+, resulting in an encoding that is both more compact and efficient for planning. We prove the correctness of the new encoding by establishing an isomorphism between the solution plans of SASE and that of STRIPS based encodings. We further analyze the transition variables newly introduced in SASE to explain why it accommodates modern SAT solving algorithms and improves performance. We give empirical statistical results to support our analysis. We also develop a number of techniques to further reduce the encoding size of SASE, and conduct experimental studies to show the strength of each individual technique. Finally, we report extensive experimental results to demonstrate significant improvements of SASE over the state-of-the-art STRIPS based encoding schemes in terms of both time and memory efficiency.