Planning as satisfiability is a universal planning framework

which translates the classical planning problem to a series of satisfiability problems

and then solves them using different kinds of excellent SAT deciders.Almost all the existing propositional encoding methods based on planning as satisfiability include a mass of overlapped axioms and redundant axioms

which have a serious influence upon the magnitude of the corresponding encoding theories and the performance of corresponding planners.In this paper

by considering overlapped axioms via analyzing the Graphplan-based encoding

which are necessary but duplicate in the final encodings

we propose a deciding strategy to reduce them.By considering redundant axioms

which are useless in the final encodings

it proposes a deleting strategy to reduce them.The soundness and completeness of proposed strategies are justified.By implementing this reduction and comparing with SATPLAN2006 planner

the experimental results demonstrate that the above strategies can effectively reduce the magnitude of objective encodings without degrading the planning efficiency.Furthermore

a deciding strategy of overlapped axioms via analyzing the state-based encoding is proposed and its soundness and completeness are also justified.The above reduction strategies can also make it possible to improve the potential power of handling larger scale problems

easier to remove redundant axioms

rather than reshaping the whole knowledge base.