基于环型扩展推理规则的MaxSAT完备算法

摘要

最大可满足性问题(MaxSAT)是可满足性问题的优化求解问题,是经典的NP难问题.基于分支限界的MaxSAT完备算法采用推理规则、失败文字检测等方法缩短算法计算时间.推理规则产生的新子句可以构成更多的冲突集,从而有效地提高了二叉树的剪枝率和算法性能.在已有的工作基础上,针对环型结构冲突集进行分析,找到与步长大于2的环型结构冲突集等价的新子句集,并利用整数规划证明了新子句集和冲突集的MaxSAT等价性.该环型扩展推理规则产生的新3元子句亦可以提高冲突集数,提高下界.在Maxsatz2013算法的基础上实现了新算法Maxsatce.测试了MaxSAT竞赛4个类别算例集.实验结果表明环型扩展推理规则对子句长度大于等于3的MaxSAT问题,可以提高二叉树分支点的下界值,最终有效地缩减算例运算时间.