Spring 2023

Extended Reunion: Satisfiability

Mar. 13May 12, 2023

This extended reunion is for long-term participants in the program Satisfiability: Theory, Practice, and Beyond, held in the spring 2021 semester. It will provide an opportunity to meet old and new friends. Moreover, we hope that it will give everyone a chance to reflect on the progress made during the semester and since, and sketch in which directions the field should go in the future.

In an age of ubiquitous computing, computational complexity theory is the science that studies what problems can be efficiently solved by computation. Since the founding work of the 1970s, an influential line of research has zoomed in on NP-complete problems, with the satisfiability problem for Boolean logic formulas (SAT) at its head, which turned out to be exactly the right notion to capture literally thousands of important applied problems in different fields. Based on the assumption of the hardness of NP, whose validity is one of the famous Millennium Prize Problems, a rich mathematical theory has been developed for establishing conditional results that state that all these problems are infeasible to solve, in the worst case.

The trouble is that real problems are not worst-case. The last two decades have seen the development of exceedingly efficient algorithms for many of these problems, perhaps most impressively in the form of so-called SAT solvers for logic formulas. Traditional complexity analysis claiming exponential lower bounds is arguably not very relevant in this setting, but this also means that we lack tools to understand how these algorithms can perform so well and why they sometimes spectacularly fail.

This program will bring together leading theoreticians and practitioners that work on SAT and its generalizations, and approach it from all possible angles: complexity theory, logic, computational algebra, optimization, SAT solving, constraint programming, random instances, SAT modulo theories (SMT), etc. The goal is to develop a better mathematical understanding of real-world efficient computation, and to work towards further algorithmic progress on problems that are currently beyond reach. So far, theoretical and applied research in these areas has developed mostly separately, but several joint workshops in recent years showed that the communities are eager for more interaction. This program is hence an opportunity for a longer-term collaboration and exchange of ideas between theoreticians and practitioners, that has potential for significant long-term impact in mathematics, computer science, and industry. This semester program could provide a decisive contribution in building a joint community of researchers working on constructing efficient algorithms and analyzing the computational complexity of applied problems.

Click here to subscribe to our news and events to learn more about this and other events.


Albert Atserias (Universitat Politècnica de Catalunya), Sam Buss (UC San Diego), Vijay Ganesh (University of Waterloo), Antonina Kolokolova (Memorial University of Newfoundland), Jakob Nordström (University of Copenhagen & Lund University)

Long-Term Participants (including Organizers):

Albert Atserias (Universitat Politècnica de Catalunya), Paul Beame (University of Washington), Olaf Beyersdorff (Friedrich-Schiller University of Jena), Nikolaj Bjorner (Microsoft Research), María Luisa Bonet Carbonell (Universitat Politècnica de Catalunya), Sam Buss (UC San Diego), Supratik Chakraborty (IIT Bombay), Susanna de Rezende (Lund University), Katalin Fazekas (TU Wien), Johannes Fichte (TU Wien), Noah Fleming (Memorial University), Vijay Ganesh (University of Waterloo), Marijn Heule (Carnegie Mellon University), Russell Impagliazzo (UC San Diego), Matti Järvisalo (University of Helsinki), Valentine Kabanets (Simon Fraser University), Phokion G. Kolaitis (UC Santa Cruz and IBM Research), Antonina Kolokolova (Memorial University of Newfoundland), Massimo Lauria (Sapienza - Università di Roma), Daniel Le Berre (CRIL-CNRS Université d'Artois), Jordi Levy Diaz (Artificial Intelligence Research Institute, Spanish National Research Council), Meena Mahajan (Institute of Mathematical Sciences), Ciaran McCreesh (University of Glasgow), Kuldeep Singh Meel (National University of Singapore), Sibylle Möhle (Max Planck Institute for Informatics), Jakob Nordström (University of Copenhagen & Lund University), Joanna Ochremiak (CNRS), Toni Pitassi (Columbia University), Pavel Pudlák (Czech Academy of Sciences), Rahul Santhanam (University of Oxford), Laurent Simon (Bordeaux INP), Stefan Szeider (TU Wien), Marc Vinyals (Memorial University), Ryan Williams (MIT)

Visiting Graduate Students and Postdocs:

Benjamin Böhm (Friedrich-Schiller University of Jena), Marlene Gründel (Friedrich-Schiller University of Jena), Hecher Markus (TU Wien), Matthew McIlree (University of Glasgow)


Monday, Mar. 27Wednesday, Mar. 29, 2023


Antonina Kolokolova (Memorial University of Newfoundland; chair), Paul Beame (University of Washington), Jeff Edmonds (York University), Ian Mertz (University of Toronto), Robert Robere (McGill University)
Monday, Apr. 17Friday, Apr. 21, 2023