Parallel variable elimination on CNF formulas

Abstract

Formula simplification is important for the performance of SAT solvers. However, when applied until completion, powerful preprocessing techniques like variable elimination can be very time consuming. Therefore, these techniques are usually used with a resource limit. Although there has been much research on parallel SAT solving, no attention has been given to parallel preprocessing. In this paper we show how the preprocessing techniques subsumption, clause strengthening and variable elimination can be parallelized. For this task either a high-level variable-graph formula partitioning or a fine-grained locking schema can be used. By choosing the latter and enforcing clauses to be ordered, we obtain powerful parallel simplification algorithms. Especially for long preprocessing times, parallelization is beneficial, and helps Minisat to solve 11 % more instances of recent competition benchmarks. © 2013 Springer-Verlag Berlin Heidelberg.