Abstract: As an important preprocessing algorithm, variable elimination algorithm has been applied to a variety of preprocessors. By comparing and studying variable elimination resolution algorithm’ influence of the preprocessing and solving process under different constraint conditions, this paper proposes a variable elimination resolution algorithm based on dynamic constraint of literal size. This algorithm only allows performing variable elimination replacement operation when the length of clauses after resolved is less than that of original one. Depending on that, this paper achieves a preprocessor based on MiniSat open source for satisfiability problems—MiniSat BFS. Finally, the experimental results show that, compared with the existing algorithm, the improved algorithm not only reduces the number of clauses, variables and characters, but also shortens the runtime of preprocessor and solver for industrial instances. It is worth mentioning that new algorithm can solve more instances within limited time.

Key words: satisfiability problem, variable elimination resolution, MiniSat

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

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