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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
SAT and SMT ITACAS at SUN I
Chair(s): Lijun Zhang Chinese Academy of Sciences
10:30
30m
Talk
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
30m
Talk
Parallel SAT Simplification on GPU Architectures
TACAS
Muhammad Osama Eindhoven University of Technology, Anton Wijs Eindhoven University of Technology
Link to publication
11:30
30m
Talk
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
30m
Talk
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