Parallel SAT Simplification on GPU Architectures
The growing scale of applications encoded to Boolean Satisfiability (SAT) problems imposes the need for accelerating SAT simplifications or preprocessing. Parallel SAT preprocessing has been an open challenge for many years. Therefore, we propose novel parallel algorithms for variable and subsumption eliminations targeting Graphics Processing Units (GPUs). We implemented the new algorithms in a tool called SIGmA. Benchmarks show that SIGmA achieves an acceleration of 66x over a state-of-the-art SAT simplifier (SatELite). Regarding SAT solving, we have conducted a thorough evaluation, comparing SIGmA in combination with MiniSat to SatELite, and studying the impact of SiGmA on the solvability of Lingeling. We conclude that our algorithms have a considerable impact on the solvability of SAT problems.
Mon 8 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | |||
10:30 30mTalk | Decomposing Farkas Interpolants TACAS Martin Blicha USI Lugano, Switzerland, Antti Hyvärinen , Jan Kofroň Charles University, Natasha Sharygina USI Lugano, Switzerland Link to publication | ||
11:00 30mTalk | Parallel SAT Simplification on GPU Architectures TACAS Link to publication | ||
11:30 30mTalk | Encoding Redundancy for Satisfaction-Driven Clause LearningBest paper nomination TACAS Marijn Heule The University of Texas at Austin, Benjamin Kiesl CISPA Helmholtz Center for Information Security, Armin Biere Johannes Kepler University Linz Link to publication | ||
12:00 30mTalk | WAPS: Weighted and Projected Sampling TACAS Rahul Gupta , Shubham Sharma , Subhajit Roy IIT Kanpur, India, Kuldeep S. Meel National University of Singapore Link to publication |