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

摘要：

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

关键词：可满足性问题、变量分解消除、MiniSat

分类号：TP301(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant Nos.61373035,61373165,61070202,61100049;the National High Technology Research and Development Program of China under Grant No.2013AA013204国家高技术研究发展计划863计划;the Special Fund for Fast Sharing of Science Paper in Net Era by CSTD under Grant No.2012008

在线出版日期：2014-11-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：1314-1323