Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas

摘要

We present an improvement to the HYPRE preprocessing algorithm that was suggested by Bacchus and Winter in SAT 2003. Given the power of modern SAT solvers, HYPRE 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 HYPRE, is much more efficient. Experiments on a large set of industrial Benchmark sets from previous SAT competitions show that HYPERBINFAST is always faster than HYPRE (sometimes an order of magnitude faster on some of the bigger CNP 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.