Effective preprocessing in SAT through variable and clause elimination.

*(English)* Zbl 1128.68463
Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 61-75 (2005).

Summary: 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.

##### MSC:

68T20 | AI problem solving (heuristics, search strategies, etc.) |

68T15 | Theorem proving (deduction, resolution, etc.) |