SIGmA: GPU Accelerated Simplification of SAT Formulas

摘要

We present SIGmA (SAT sImplification on GPU Architectures), a preprocessor to accelerate SAT solving that runs on NVIDIA GPUs. We discuss the tool, focussing on its full functionality and how it can be used in combination with state-of-the-art SAT solvers. SIGmA performs various types of simplification, such as variable elimination, subsumption elimination, blocked clause elimination and hidden redundancy elimination. We study the effectiveness of our tool when applied prior to SAT solving. Overall, for our large benchmark set of problems, SIGmA enables MiniSat and Lingeling to solve many problems in less time compared to applying the SatElite preprocessor.