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

来源：计算机集成制造系统杂志2020年第8期北京时间：

作者：宁欣然,徐扬,陈振颂

单位：1.西南民族大学计算机科学与技术学院2.西南交通大学系统可信性自动验证国家地方联合工程实验室3.武汉大学土木建筑工程学院

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

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

基金资助：国家自然科学基金资助项目(61673320,71801175);西南民族大学中央高校基本科研业务费专项资金项目资助(2020NQN40);中央高校基本科研业务费专项资金资助项目(2682018ZT10,2042018kf0006);香港特别行政区研究资助委员会资助项目(T32-101/15-R)。