Dagstuhl Seminar 22411
Theory and Practice of SAT and Combinatorial Solving
( Oct 09 – Oct 14, 2022 )
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/22411
Organizers
- Olaf Beyersdorff (Friedrich-Schiller-Universität Jena, DE)
- Armin Biere (Universität Freiburg, DE)
- Vijay Ganesh (University of Waterloo, CA)
- Jakob Nordström (University of Copenhagen, DK & Lund University, SE)
Contact
- Michael Gerke (for scientific matters)
- Christina Schwarz (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
The Boolean satisfiability (SAT) problem plays a fascinating dual role in computer science. By the theory of NP-completeness, this problem captures thousands of important applications in different fields, and a rich mathematical theory has been developed showing that all these problems are likely to be infeasible to solve in the worst case. But real-world problems are typically not worst-case, and in recent decades exceedingly efficient algorithms based on so-called conflict-driven clause learning (CDCL) have turned SAT solvers into highly practical tools for solving large-scale real-world problems in a wide range of application areas. Analogous developments have taken place for problems beyond NP such as SAT-based optimization (MaxSAT), pseudo-Boolean optimization, satisfiability modulo theories (SMT) solving, quantified Boolean formula (QBF) solving, constraint programming, and mixed integer programming, where the conflict-driven paradigm has sometimes been added to other powerful techniques.
The current state of the art in combinatorial solving presents a host of exciting challenges at the borderline between theory and practice. Can we gain a deeper scientific understanding of the techniques and heuristics used in modern combinatorial solvers and why they are so successful? Can we develop tools for rigorous analysis of the potential and limitations of these algorithms? Can computational complexity theory be extended to shed light on real-world settings that go beyond worst case? Can more powerful methods of reasoning developed in theoretical research be harnessed to yield improvements in practical performance? And can state-of-the-art combinatorial solvers be enhanced to not only solve problems, but also provide verifiable proofs of correctness for the solutions they produce?
In this Dagstuhl Seminar, we aim to gather leading applied and theoretical researchers working on SAT and combinatorial optimization more broadly in order to stimulate an exchange of ideas and techniques. We see great opportunities for fruitful interplay between theory and practice in these areas, as well as for technology transfer between different paradigms in combinatorial optimization, and believe that a more vigorous interaction has potential for major long-term impact in computer science, as well for applications in industry.
Creative Commons BY 4.0
Olaf Beyersdorff, Armin Biere, Vijay Ganesh, and Jakob Nordström
- Jeremias Berg (University of Helsinki, FI)
- Olaf Beyersdorff (Friedrich-Schiller-Universität Jena, DE) [dblp]
- Armin Biere (Universität Freiburg, DE) [dblp]
- Nikolaj S. Bjørner (Microsoft - Redmond, US) [dblp]
- Bart Bogaerts (VU - Brussels, BE)
- Benjamin Böhm (Friedrich-Schiller-Universität Jena, DE)
- Jonas Conneryd (Lund University, SE)
- Susanna de Rezende (Lund University, SE) [dblp]
- Katalin Fazekas (TU Wien, AT)
- Mathias Fleury (Universität Freiburg, DE) [dblp]
- Vijay Ganesh (University of Waterloo, CA) [dblp]
- Mexi Gioni (Zuse Institut Berlin, DE)
- Ambros M. Gleixner (HTW - Berlin, DE) [dblp]
- Malte Helmert (Universität Basel, CH) [dblp]
- Marijn J. H. Heule (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Mikoláš Janota (Czech Technical University - Prague, CZ) [dblp]
- Matti Järvisalo (University of Helsinki, FI) [dblp]
- Daniela Kaufmann (TU Wien, AT) [dblp]
- Antonina Kolokolova (University of Newfoundland, CA) [dblp]
- Laura Kovács (TU Wien, AT) [dblp]
- Chunxiao (Ian) Li (University of Waterloo, CA)
- Meena Mahajan (The Institute of Mathematical Sciences - Chennai, IN) [dblp]
- Ciaran McCreesh (University of Glasgow, GB)
- Kuldeep S. Meel (National University of Singapore, SG) [dblp]
- Jakob Nordström (University of Copenhagen, DK & Lund University, SE) [dblp]
- Andy Oertel (Lund University, SE)
- Albert Oliveras (UPC Barcelona Tech, ES) [dblp]
- Pavel Pudlák (The Czech Academy of Sciences - Prague, CZ) [dblp]
- Torsten Schaub (Universität Potsdam, DE) [dblp]
- Andre Schidler (TU Wien, AT)
- Laurent Simon (University of Bordeaux, FR) [dblp]
- Friedrich Slivovsky (TU Wien, AT) [dblp]
- Martin Suda (Czech Technical University - Prague, CZ) [dblp]
- Stefan Szeider (TU Wien, AT) [dblp]
- Yong Kiam Tan (Infocomm Research - Singapore, SG)
- Dieter Vandesande (VU - Brussels, BE)
- Marc Vinyals (University of Newfoundland, CA) [dblp]
- Ryan Williams (MIT - Cambridge, US) [dblp]
- Emre Yolcu (Carnegie Mellon University - Pittsburgh, US)
Related Seminars
- Dagstuhl Seminar 15171: Theory and Practice of SAT Solving (2015-04-19 - 2015-04-24) (Details)
Classification
- Computational Complexity
- Data Structures and Algorithms
- Logic in Computer Science
Keywords
- Boolean satisfiability
- SAT solving
- computational complexity
- proof complexity
- combinatorial optimization
