Encoding Redundancy for Satisfaction-Driven Clause LearningBest paper nomination
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 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 |