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

Satisfaction-Driven Clause Learning (SDCL) is a recent SAT solving paradigm that aggressively trims the search space of possible truth assignments. To determine whether the SAT solver is currently exploring a dispensable part of the search space, SDCL makes use of the so-called positive reduct of a formula: The positive reduct is an easily solvable propositional formula that is satisfiable if the current assignment of the solver can be safely pruned from the search space. In this paper, we present two novel variants of the positive reduct that allow for even more aggressive pruning. Using one of these variants allows SDCL to solve harder problems, in particular the well-known Tseitin formulas. For the first time, we were able to generate and automatically check clausal proofs of these 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