关键词: 子句消去方法, 命题逻辑可满足性问题求解, 蕴涵模归结, 规划问题

Abstract: Aiming at the clause redundancy problem caused by transforming intelligent planning problems such as production line scheduling,aircraft planning and scheduling,assembly planning and plant process planning into propositional satisfiability problems,three clause elimination methods were proposed to simplify those propositional formulas from planning problems.Through making dimension reduction to propositional logic by Implication Modulo Resolution (IMR) in first-order logic,IMR on propositional logic was established,and the redundant feature of propositional logic clause was discussed.Under the principle of IMR,three types of novel clause elimination methods that were (BC+RS)E,(RS+RHT)E and (RHS+RHT)E were proposed,which were compared with Blocked Clause Elimination (BCE).The result showed that when coping with propositional formulas with a large variety of clauses transformed from realistic planning problems,the effects of simplifying formulas of novel clause elimination methods were better with longer limit time.Within the same runtime,the capability of simplifying of clause elimination methods would be the best when if there was a balance between the complexity of clause elimination methods identification condition and its time complexity.While dealing with the simpler formulas generated randomly,the more effective the clause elimination method was,the better its capability to simplify.

Key words: clause elimination method, propositional satisfiability solving, implication modulo resolution, planning problem