摘要：基于可满足性的规划方法通过将经典规划问题转换为一系列可满足性问题进行求解.几乎所有基于可满足性的规划编码都存在着大量的重叠公理和冗余公理,直接决定了编码理论的编码大小与求解难度.通过分析基于Graphplan的编码方式,分别提出了重叠公理的判定策略和冗余公理的删除策略.在SATPLAN2006规划系统中实现相应的编码方式并与原系统进行比较,实验结果表明：该约简方法能够在不降低规划性能的前提下有效地压缩转换理论的编码大小.通过分析基于状态的编码方式,提出了重叠公理的判定策略.重叠公理与冗余公理的约简容易实现,且并未改变知识库的结构模式,为进一步提高规划系统处理更大规模问题的能力提供了可能.

关键词：智能规划 基于可满足性的规划 命题逻辑 公理约简 编码 

单位：吉林大学计算机科学与技术学院; 吉林长春130012; 吉林大学符号计算与知识工程教育部重点实验室; 吉林长春130012; 吉林大学数学学院; 吉林长春130012