Effective preprocessing in SAT through variable and clause elimination
Effective preprocessing in SAT through variable and clause elimination
复制标题
DOI：
10.1007/11499107_5
复制
发表时间：
2005-01-01
期刊：
影响因子：
--
通讯作者：
Biere, A
中科院分区：
文献类型：
--
作者：
Eén, N;Biere, A
对SAT实例进行预处理可以显著减小其大小。我们将变量消去与包含和自包含归结相结合，证明了这些技术不仅比以往基于变量消去的前处理方法进一步缩小了公式，而且对于典型的工业SAT问题，大大减少了SAT求解器的运行时间。我们讨论了关键的实施细节，以使削减过程足够快，从而使其切实可行。
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.