Combination and Designation of Axioms in Proposional Encodings
Shi Jing-jing · 2009
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 SATPLAN2006 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 SATPLAN2006 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.