基于命题可满足性的经典最优规划方法

基于graphplan的编码方式是2006年国际规划竟赛中著名的最优规划系统satplan2006采用的编码方式。首先给出与编码相关的概念与性质，在基于graphplan的编码方式的基础上，设计一种新的编码方式:基于fa的编码方式，并从理论上证明该编码方式的有效性。设计并实现对应的规划系统fa-sp，利用国际规划竞赛选用的benchmark问题予以测试。实验结果表明，与satplan2006相比，fa-sp对于所测两类规划域编码规模均有所压缩，除个别问题外求解效率都有一定程度的提高;对于顺序规划域bloc