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

MaxSAT complete algorithm based cycle extended inference rules

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

Maximum Satisfiability problem（MaxSAT）is a classic optimization problem and NP-hard problem.Many NP problems can be transformed into MaxSAT problems,and many industrial problems are solved by MaxSAT algorithms effectively.Improved technologies and data structure proposed in recent years led to solve much larger instance than before.MaxSAT exact algorithm based on branch and bounds used inference rules and failed literal detection to reduce the running time.Inference rules proposed in the past time obeyed the equivalence of MaxSAT problem.Compared to not using inference rules,new clauses in clause set created by inference rules can deduce more conflict sets and improve binary tree pruning rate and algorithm＇s performance.Inference rules fund equivalent clauses for chain structure or cycle structure of conflict clause set.Through the analysis of cycle conflict set whose step length is greater than two,we find the new equivalent clause sets with them.The equivalent proof about new clause sets and conflict sets was described in this article.Therefore,new cycle extend inference rules were proposed to improve lower bounds and reduce the running time in further.Integer programming proved the soundness of new cycle extend inference rule.New algorithm Maxsatce adopted new rules and worked on the base of Maxsatz2013.Experiments tested four types MaxSAT instances from the website of MaxSAT competition.The experimental resultsshowed cycle extend inference rules could improve the lower bounds at binary tree branch when solving instance＇s clause length was greater than or equal to three.Experiment result showed cycle extend inference rule can work well when search level was close to middle of search tree.Running time of random instances and crafted instances can reduce at least 3%~14%.