CAJ | 학술논문

变量消除算法作为一种重要的预处理算法已经应用于多种预处理器中。对比研究了在不同约束条件下，变量消除算法对简化性能和求解性能的影响，提出了基于子句文字长度动态约束的变量消除算法。该算法只允许当变量分解后的子句文字长度比原有子句文字少时，执行变量消除替换操作。在此基础上实现了一个基于MiniSat开源代码的可满足性问题预处理器MiniSat BFS。实验结果表明，与现有的基于子句数目约束的算法相比，新算法不仅降低了子句、变量和文字的数目，而且缩短了预处理过程和求解过程的时间消耗。更重要的是，改进后的算法在限定时间内可以求解更多的可满足性问题。
변량소제산법작위일충중요적예처리산법이경응용우다충예처리기중。대비연구료재불동약속조건하，변량소제산법대간화성능화구해성능적영향，제출료기우자구문자장도동태약속적변량소제산법。해산법지윤허당변량분해후적자구문자장도비원유자구문자소시，집행변량소제체환조작。재차기출상실현료일개기우MiniSat개원대마적가만족성문제예처리기MiniSat BFS。실험결과표명，여현유적기우자구수목약속적산법상비，신산법불부강저료자구、변량화문자적수목，이차축단료예처리과정화구해과정적시간소모。경중요적시，개진후적산법재한정시간내가이구해경다적가만족성문제。
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 algo-rithm based on dynamic constraint of literal size. This algorithm only allows performing variable elimination replace-ment 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 indus-trial instances. It is worth mentioning that new algorithm can solve more instances within limited time.