依赖公理约简的经典规划方法

摘要

Planning as satisfiability is a universal planning framework, which translates the classical planning problem to a series of satisfiability problems,and then solves them using different kinds of excellent SAT deciders. Almost all the existing propositional encoding methods based on planning as satisfiability include a mass of overlapped axions and redundant axioms,which have a serious influence upon the magnitude ofthe corresponding encoding theodes and the performance of corresponding planners. In this paper,by considering overlapped axioms via analyzing the Graphplan-based encoding,which are ncessary but duplicate in the final encoxtings, we propose a deciding strategy to reduce them. By considering redundant axioms, which are useless in the final encodings,it proposes a deleting strategy to reduce them. The soundness and completeness of proposed strategies are justified. By implementing this reduction and comparing with SATPLAN2006 planner, the experimental results demonstrate that the above strategies can effectively reduce the magnitude of objective encodings without degrading the planning efficiency. Furthennore, a deciding strategy of overlapped axioms via analyzing the state-based encoding is proposed and its soundness and completeness are also justified.The above reduction strategies can also make it possible to improve the potential power of handling larger scale problems, easier to remove redundant axioms,rather than reshaping the whole knowledge base.%基于可满足性的规划方法通过将经典规划问题转换为一系列可满足性问题进行求解.几乎所有基于可满足性的规划编码都存在着大量的重叠公理和冗余公理,直接决定了编码理论的编码大小与求解难度.通过分析基于Graphplan的编码方式,分别提出了重叠公理的判定策略和冗余公理的删除策略.在SATPLAN2006规划系统中实现相应的编码方式并与原系统进行比较,实验结果表明:该约简方法能够在不降低规划性能的前提下有效地压缩转换理论的编码大小.通过分析基于状态的编码方式,提出了重叠公理的判定策略.重叠公理与冗余公理的约简容易实现,且并未改变知识库的结构模式,为进一步提高规划系统处理更大规模问题的能力提供了可能.