Abstract
Presenter: Benjamin Kiesl
Time: 8:30 - 9:10
Title: Preprocessing in SAT Solving
: Preprocessing is a key component of the Boolean satisfiability (SAT) solving workflow. In practice, preprocessing techniques aim at simplifying Boolean formulas to speed up the search subsequently performed by a SAT solver. In this talk, I discuss the ideas behind preprocessing as well as some of the most successful preprocessing techniques used by modern solvers.
Presenter: Jeremias Berg
Time: 9:10 - 9:50
Title: From decisions to optimization - preprocessing in MaxSAT Solving
: Maximum satisfiability (MaxSAT) is an optimization version of Boolean satisfiability (SAT). Constituting a declarative approach to optimization, modern state-of-the-art MaxSAT solvers allow tackling various NP-hard combinatorial optimization problems via simple propositional encodings. In recent years MaxSAT has matured into an effective alternative to e.g. the classical declarative optimization paradigm of integer programming (IP), especially in domains where the underlying constraints are naturally represented with logical constraints. In this talk, I will give an overview of the various reasoning and simplification techniques employed by state-of-the-art MaxSAT solvers, including how to lift deduction techniques from the domain of Boolean Satisfiability solving to MaxSAT. I will also talk about our preliminary work on a theoretical foundation of preprocessing in MaxSAT and highlight further research directions.
Presenter: Martina Seidl
Time: 9:50 - 10:30
Title: Preprocessing for Quantified Boolean Formulas
: Quantified Boolean formulas (QBF) are well suited to encode many application problems from artificial intelligence, formal verification, and synthesis. Over the last years, it has become evident that preprocessing is crucial to exploit structural information that is indispensable for fast solving. In this talk, we review preprocessing techniques implemented in modern preprocessors and show how the correctness of the rewritings performed by a preprocessor can be validated with the help of the QRAT proof system.