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

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