Satisfiability: Theory, Practice, and Beyond

The Boolean satisfiability (SAT) problem plays a key role in computer science, with major implications for both theoretical and practical research. SAT captures thousands of important applications in different fields, which, by the theory of NP-completeness, are all widely believed to be impossible to solve efficiently in the general case. At the same time, dramatic improvements in applied algorithms over the last decades have led to so-called SAT solvers that perform exceedingly well in practice. There have been similar developments for other combinatorial solving paradigms beyond NP such as MaxSAT and pseudo-Boolean optimization, satisfiability modulo theories (SMT) solving, constraint programming, and mixed integer linear programming.

This state of affairs presents a rich palette of problems at the intersection of theory and practice. Can we gain a rigorous understanding of the performance of modern combinatorial solvers, opening up avenues for further advances? Can we provide a mathematical analysis of the underlying methods of reasoning and delineate their potential and limitations? Can computational complexity theory shed light on “real-world computation” beyond the worst-case setting? Can theoretically more powerful methods be harnessed to yield dramatically faster combinatorial solvers also in practice? And can state-of-the-art combinatorial solvers be modified to not only solve problems, but also provide machine-verifiable proofs of correctness for results they compute?

In this workshop, we aim to collect leading researchers from theoretical and applied research areas related to SAT and combinatorial optimization more broadly in order to discuss these and other questions, and to stimulate an exchange of ideas and techniques.