基于扩展失败文字检测的MaxSAT完备算法

MaxSAT complete algorithm based on extended failed literal detection

为提高MaxSAT完备算法剪枝率和运算效率,分析失败文字检测寻找冲突集的过程,提出扩展失败文字检测方法。通过延长失败文字搜索冲突的路径,形成搜索1步、2步和任意步的递进失败文字检测方式,实现改进的MaxsatzEF算法。实验测试了MaxSAT国际竞赛4个类别的500多个算例,实验结果表明,递进失败文字检测方法找到了更多独立冲突集,可有效提高算法的下界,大幅缩短复杂算例的运行时间。

To improve prune rate and running time of maximum satisfiability problem（MaxSAT problem）algorithms,the searching process of failed literal detection for conflicted sets was analyzed.Extended failed literal detection was proposed to increase the rooting of search conflict in inference graph,climactic way was executed by searching one step,two steps and any steps.The improved MaxsatzEF algorithm was then realized.More than five hundred MaxSAT instances from MaxSAT evaluation competition benchmark in four different MaxSAT problem types were tested.Experimental results show that progressive failed literal detection find more independent conflict sets,which increases the lower bounds effectively and cuts off running time to a great extent for complicated instance at last.