Abstract: Graphplan-based encoding is a novel encoding adopted by SATPLAN2006,which is the statcof-thcart optimal planner of International Planning Competition in 2006. It firstly defined the concepts and characters about encoding.Based on Graphplan-based encoding, it proposed a new encoding, called FA-based encoding, by reducing the mutex axioms of actions and appending frame axioms. It justifies the soundness and completeness of the corresponding proposed encoding. We designed and implemented the corresponding planner called FA-SP, and tested it with benchmarks adopted by International Planning Competition, respectively. Comparing with SATPLAN2006，the results validate th at for both all two domains tested, the scales of encodings of FA-SP are compacted and solver efficiencies of them arc improved, and it is notes to sec that for sequential planning problems Blocks World, the scales of encodings of FA-SP are compacted nearly 40% and solver efficiencies of them are improved nearly 2 times; for parallel planning problems Logistics, the scales of encodings of FA-SP arc compacted more than 75%. The solver efficiencies of FA-SP are improved several times, and the scales of them are enlarged less than 5% for overwhelming majority problems.

Key words: Planning as satisfiability, Graphplan-based encoding, Encoding, Frame axiom, Planner