Muhammad Osama: SIGmA: SAT Simplifications on GPU Architecture

Event Details

The growing scale of industrial applications encoded to Boolean Satisfiability (SAT) problems imposed the researchers to practice SAT simplification as an imperative requirement for any SAT solver. In this talk, I will discuss how GPU can be utilized to perform variable and subsumption eliminations in parallel. Benchmarks show that our proposed simplifier (SIGmA) achieved an acceleration of 250x over SatELite. Regarding SAT solving, SIGmA outperformed SatELite in terms of problems solved faster when combined with MiniSat by a factor of 77%. Moreover, MiniSat was more effective than Lingeling by 73.3% in solving simplified formulas given by SIGmA.