Muhammad Osama: “SIGmA: GPU Accelerated Simplification of SAT Formulas”


Event Details


In this talk, I will present SIGmA (SAT sImplification on GPU Architectures), a preprocessor to accelerate SAT solving that runs on NVIDIA GPU(s). We discuss the tool, focusing on its full functionality, including new simplifications and multi-GPU support with load balancing mechanism. 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/Lingeling(integrated) preprocessors.