命题逻辑可满足性问题求解器的新型预处理子句消去方法

Novel preprocessing clause elimination methods for propositional SAT solvers

针对生产线调度、航空器规划和调度等规划问题转化为命题逻辑可满足性问题时带来的子句冗余问题,提出3种子句消去方法对命题逻辑可满足性问题进行子句集化简。通过将一阶逻辑上子句消去的蕴涵模归结原则降维到命题逻辑上,建立了命题逻辑上的蕴涵模归结原则,对命题逻辑子句的冗余性质进行了探讨。在该原则框架下,建立了(BCRS)E,(RSRHT)E,(RHSRHT)E 3种新的子句消去方法。将这3个子句消去方法与著名的BCE子句消去方法进行实验比照,结果表明,在化简由现实规划问题转化而来的子句数量庞大且复杂的子句集时,限定时间越长,子句消去方法化简子句集的效果越好;在同样的限定时间中,当子句消去方法的判定条件难易程度和时间复杂度达到平衡时,子句消去方法的化简能力最好;在化简随机生成的比较简单的子句集时,有效性越高的新型子句消去方法化简子句集的能力越强,且均好于BCE子句消去方法。

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(BCRS)E,(RSRHT)E and(RHSRHT)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.