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.

Invited Participants

Özgür Akgün (University of St Andrews), Albert Atserias (Universitat Politècnica de Catalunya), Otto Berg (University of Helsinki), Bart Bogaerts (Vrije Universiteit Brussel (VUB)), Randal Bryant (Carnegie Mellon University), Susanna F. de Rezende (Lund University), Rayna Dimitrova (CISPA Helmholtz Center for Information Security), Katalin Fazekas (TU Wien), Marijn Heule (Carnegie Mellon University), John Hooker (Carnegie Mellon University), Jie-Hong Roland Jiang (National Taiwan University), Daniela Kaufmann (TU Wien), Benjamin Kiesl (Helmholtz Center for Information Security (CISPA)), Donald Knuth (Stanford University), Ning Luo (Northwestern University), Ciaran McCreesh (University of Glasgow), Matthew Mcilree (University of Glasgow), Alexander Nadel (Intel), Nina Narodytska (VMware Research), Shuo Pang (University of Copenhagen), Gilles Pesant (Polytechnique Montréal), Robert Robere (McGill University), Karem Sakallah (University of Michigan), Torsten Schaub (University of Potsdam), Martina Seidl (Johannes Kepler University), Mate Soos (National University of Singapore), Stefan Szeider (TU Wien), Marc Vinyals (Memorial University), William Wesley (UC Davis)