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

摘要：

最大可满足性问题(MAXSAT)是经典的NP完全问题SAT的一个扩展问题.基于分支限界设计MAXSAT完备算法时,如何有效地提高下界是设计高效算法的关键和难点.基于优先找到规模小、结构简单的冲突集的思想,在Maxsatz算法的基础上,提出了改进的算法Maxsatz2013.通过使用推理规则优先、改变单子句的传播顺序、进一步失败文字检测这3个优化策略,增加了检测到的冲突集数,从而有效地提高了下界.测试了MAXSAT 4个类别共800多个算例.实验结果表明,这3个优化冲突集的策略是可行且有效的,所提出的算法在每一类算例上均明显地提高了计算效率.

关键词： 最大可满足性问题 算法设计 冲突集优化 系统框架

作者: 刘燕丽 李初民 何琨

作者单位: 华中科技大学计算机科学与技术学院 武汉 430074;武汉科技大学理学院 武汉 430081 亚眠大学计算机科学系 80033 法国;华中科技大学计算机科学与技术学院 武汉 430074 华中科技大学计算机科学与技术学院 武汉 430074

会议类型: 国内会议

会议名称: 2013中国计算机大会

会议地点: 长沙

会议语种:中文

页码: 2087-2095

在线出版日期: 2013-10-01（万方平台首次上网日期，不代表论文的发表时间）