ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 11:00 - 11:30 at SUN I - SAT and SMT I Chair(s): Lijun Zhang

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 Apr

tacas-2019-papers
10:30 - 12:30: TACAS 2019 - SAT and SMT I at SUN I
Chair(s): Lijun ZhangChinese Academy of Sciences
tacas-2019-papers10:30 - 11:00
Talk
Martin BlichaUSI Lugano, Switzerland, Antti Hyvärinen, Jan KofroňCharles University, Natasha SharyginaUSI Lugano, Switzerland
Link to publication
tacas-2019-papers11:00 - 11:30
Talk
Muhammad OsamaEindhoven University of Technology, Anton WijsEindhoven University of Technology
Link to publication
tacas-2019-papers11:30 - 12:00
Talk
Marijn HeuleThe University of Texas at Austin, Benjamin KieslCISPA Helmholtz Center for Information Security, Armin BiereJohannes Kepler University Linz
Link to publication
tacas-2019-papers12:00 - 12:30
Talk
Rahul Gupta, Shubham Sharma, Subhajit RoyIIT Kanpur, India, Kuldeep S. MeelNational University of Singapore
Link to publication