命题编码中公理的组合与设计

Combination and Designation of Axioms in Proposional Encodings

近年来,基于可满足性的规划方法研究逐渐成为智能规划研究领域中的热点。提出3种基于Graphplan的编码方式中公理的改进:动作互斥的部分放松、动作互斥的完全放松方法、添加框架公理。基于SATPLAN2006规划系统分别实现上述3种改进的编码方式,并对国际规划竞赛中选用的标准后勤域与积木世界域的问题样例予以测试,分析不同编码方式的编码规模与求解效率,验证了基于Graphplan编码方式的改进在绝大多数情况下是有效的。最后,实现基于状态的编码方式,并对上述两个域进行测试,比较约简动作与约简状态这两种极端方式的求解效率和编码规模。实验结果表明,在后勤域的某些问题上基于状态的编码方式比基于动作的编码方式有效得多。上述的改进策略表明,可根据问题域的特性等来考虑该问题最适宜哪些公理组合的编码方式,而不固定使用某种特定的编码方式。

In recent years, researches on planning as satisfiability have become a popular trend. We proposed partial relaxation and completed relaxation methods about mutex actions, appended the frame axioms finally. Taking SATP-LAN2006 as the base,we implemented these improved encoding methods respectively, tested them in the logistics track and the block world track which are used in international planning competition, and analyzed the encoding scale and plan efficiency of different encoding methods, and then validated the improvements based on the graphplan encoding method in the overwhelming majority situation are effective. Finally, we implemented the state-based encoding method in SATP-LAN2006 planner, tested on the above tracks and compared two extremely conditions, which eliminate actions and states respectively. The experimental results show that state-based encoding method is more effective in logistics track than action-based encoding. The above improving strategies about the SATPLAN2006 planner are proved effective, and we should decide which combination of axioms in one encoding method is most suitable by consideing the characteristics of different tracks, rather than using certain encoding method absolutely.