zbMATH — the first resource for mathematics

Cost-effective hyper-resolution for preprocessing CNF formulas. (English) Zbl 1128.68465
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, 423-429 (2005).
Summary: We present an improvement to the Hyper preprocessing algorithm that was suggested by F. Bacchus and J. Winter in SAT 2003 [“Effective preprocessing with hyper-resolution and equality reduction”, Lect. Notes Comput. Sci. 2919, 341–355 (2003)]. Given the power of modern SAT solvers, Hyper is currently one of the only cost-effective preprocessors, at least when combined with some modern SAT solvers and on certain classes of problems. Our algorithm, although it produces less information than Hyper, is much more efficient. Experiments on a large set of industrial Benchmark sets from previous SAT competitions show that HyperBinFast is always faster than Hyper (sometimes an order of magnitude faster on some of the bigger CNF formulas), and achieves faster total run times, including the SAT solver’s time. The experiments also show that HyperBinFast is cost-effective when combined with three state-of-the-art SAT solvers.
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)
BerkMin; Chaff; Siege
Full Text: DOI