基于优化冲突集提高下界的MAXSAT完备算法  

Improving Lower Bounds in MAXSAT Complete Algorithm Based Optimizing Inconsistent Set

作　　者：刘燕丽[1,2] 李初民[3,1] 何琨[1] 

机构地区：[1]华中科技大学计算机科学与技术学院,武汉430074 [2]武汉科技大学理学院,武汉430081 [3]亚眠大学计算机科学系,法国80033

出　　处：《计算机学报》2013年第10期2087-2095,共9页Chinese Journal of Computers

基　　金：国家自然科学基金(61173180;61272014)资助~~

摘　　要：最大可满足性问题(MAXSAT)是经典的NP完全问题SAT的一个扩展问题.基于分支限界设计MAXSAT完备算法时,如何有效地提高下界是设计高效算法的关键和难点.基于优先找到规模小、结构简单的冲突集的思想,在Maxsatz算法的基础上,提出了改进的算法Maxsatz2013.通过使用推理规则优先、改变单子句的传播顺序、进一步失败文字检测这3个优化策略,增加了检测到的冲突集数,从而有效地提高了下界.测试了MAXSAT 4个类别共800多个算例.实验结果表明,这3个优化冲突集的策略是可行且有效的,所提出的算法在每一类算例上均明显地提高了计算效率.Maximum Satisfiability problem （MAXSAT） is an important generalization of a classic NP-complete problem, Satisfiability problem （SAT） . The key point of designing a competitive MAXSAT complete algorithm based on branch and bounds is to improve the lower bounds effi- ciently. One unit clause can find more disjoint inconsistent sets by unit propagation. Based on the Maxsatz algorithm proposed in 2010, we propose an improved Maxsatz2013 algorithm by finding smaller disioint inconsistent sets or these inconsistent sets with simpler structures first. The algorithm adopts three optimization strategies： inference rules in priority, changing the order of unit clause propagation and further detecting failed literals. These three strategies make the detection of unit clause propagation find more disjoint inconsistent sets and hence improve the lower bounds. More than eight hundred MAXSAT instances of four different MAXSAT problem types are tested. Experimental results show the feasibility and effectiveness of the proposed algorithm, as it reduced the computation to a great extent.

关 键 词：NP完全 最大可满足性问题 单子句传播 推理规则 失败文字 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]