zbMATH — the first resource for mathematics

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.
For the entire collection see [Zbl 1077.68002].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
MiniSat; NiVER; Quantor; ZRes
Full Text: DOI