Effective preprocessing in SAT through variable and clause elimination

被引：292

作者：

Eén, N ^{[1
]}

Biere, A

机构：

[1] Chalmers Univ Technol, S-41296 Gothenburg, Sweden

[2] Johannes Kepler Univ, A-4040 Linz, Austria

来源：

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS | 2005年 / 3569卷

关键词：

D O I：

10.1007/11499107_5

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Preprocessing SAT instances can reduce their size considerably. We combine variable elimination with subsumption and self-subsuming resolution, and show that these techniques not only shrink the formula further than previous preprocessing efforts based on variable elimination, but also decrease runtime of SAT solvers substantially for typical industrial SAT problems. We discuss critical implementation details that make the reduction procedure fast enough to be practical.

引用

页码：61 / 75

页数：15