基于子句文字长度动态约束的变量消除算法

• 作者: 冯志勇 王鑫 邓晓瑶 饶国政
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 可满足性问题 变量分解消除 MiniSat
• 年，卷（期）: 2014,（11）
• 所属期刊栏目: 学术研究
• 页码范围: 1314-1323
• 页数: 10页
• 分类号: TP301
• 字数: 6300字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1405030

摘要

变量消除算法作为一种重要的预处理算法已经应用于多种预处理器中。对比研究了在不同约束条件下，变量消除算法对简化性能和求解性能的影响，提出了基于子句文字长度动态约束的变量消除算法。该算法只允许当变量分解后的子句文字长度比原有子句文字少时，执行变量消除替换操作。在此基础上实现了一个基于MiniSat开源代码的可满足性问题预处理器MiniSat BFS。实验结果表明，与现有的基于子句数目约束的算法相比，新算法不仅降低了子句、变量和文字的数目，而且缩短了预处理过程和求解过程的时间消耗。更重要的是，改进后的算法在限定时间内可以求解更多的可满足性问题。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	冯志勇	天津大学计算机科学与技术学院	146	1072	17.0	24.0
3	饶国政	天津大学计算机科学与技术学院	26	149	8.0	10.0
5	王鑫	天津大学计算机科学与技术学院	56	364	10.0	16.0
7	邓晓瑶	天津大学计算机科学与技术学院	1	7	1.0	1.0