- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
The propositional satisfiability problem (SAT) is one of the most fundamental problems in computer science. As the first problem shown to be NP-complete by the Cook-Levin Theorem, SAT remains a fundamental benchmark problem for complexity theory. In contrast to its theoretical hardness, research over the last 20 years has successfully designed and engineered powerful algorithms for the SAT problem, called SAT solvers, that are surprisingly efficient on problem instances that arise from real-world applications. However, to solve a problem with a SAT solver or a related tool, one must first formulate the problem in terms of propositional logic to be digestible by the solver. This translation from the original problem to propositional logic is often referred to as a SAT encoding. It turned out that the encoding itself is often the crucial part that determines whether the problem can be solved efficiently by the solver or not, making the encoding techniques at least as important as the solving techniques. Hence, over the last years, much effort has been put into researching efficient encoding techniques. This Dagstuhl Seminar will provide the opportunity for an in-depth discussion of the state-of-the-art of encodings and future challenges and research avenues.
More concretely, the following topics will be discussed at the seminar.
- The Effectiveness of Encodings. Current challenging research questions are new encodings for global constraints, theoretical lower and upper bounds on encoding size for global constraints, and new methods for symmetry breaking. Topics of interest are general principles of problem reformulations and their impact on the effectiveness of encodings.
- The Complexity of Encodings. Although state-of-the-art SAT solvers can deal with millions of clauses and variables, the size of the original instance must be significantly smaller since the encoding often causes a polynomial (often cubic or worse) size blow-up. At the proposed seminar, several new methods for overcoming these limitations will be discussed.
- Encoding Tools. To fully exploit the power of SAT solvers, researchers have designed high-level languages that are amenable to describing constraints and developed compilers for converting constraints into CNF. Exciting topics for discussions at the seminar include the questions of how to obtain an optimal hybridization of encodings and how to decompose global constraints.
- Lazy Encodings. An interesting approach to SAT encodings is to start with an incomplete under-constrained encoding and add clauses to it once a solution has been found that violates properties that are not considered by the encoding. SAT modulo Theories and Lazy Clause Generation are among the approaches utilizing eager encodings that will be discussed.
- Verifying Encodings. Trust in the correctness of SAT solving results increased significantly in the last couple of years as all top-tier solvers can produce proofs of unsatisfiability that can be validated using efficient and formally-verified tools. An interesting topic for the seminar is how the encoding part of the tool chain can be sufficiently validated.
- Beyond SAT. The success of SAT solving has spawned the development of efficient solvers for problems that are more general than SAT, including MaxSAT, QBF-SAT, PB, ASP, and CP. At the seminar, the different encoding techniques for these more general problems will be discussed.
- Carlos Ansotegui (University of Lleida, ES) [dblp]
- Jeremias Berg (University of Helsinki, FI)
- Olaf Beyersdorff (Friedrich-Schiller-Universität Jena, DE) [dblp]
- Armin Biere (Universität Freiburg, DE) [dblp]
- Curtis Bright (University of Windsor, CA) [dblp]
- Cayden Codel (Carnegie Mellon University - Pittsburgh, US)
- Michael Codish (Ben Gurion University - Beer Sheva, IL) [dblp]
- Ronald de Haan (University of Amsterdam, NL) [dblp]
- Emir Demirovic (TU Delft, NL)
- Andreas Falkner (Siemens AG - Wien, AT) [dblp]
- Johannes Klaus Fichte (Linköping University, SE)
- María Andreína Francisco Rodríguez (Uppsala University, SE)
- 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]
- George Katsirelos (INRAE - Palaiseau, FR)
- Daniela Kaufmann (TU Wien, AT) [dblp]
- Markus Kirchweger (TU Wien, AT)
- Zeynep Kiziltan (University of Bologna, IT)
- Inês Lynce (University of Lisbon, PT)
- Vasco Manquinho (INESC-ID - Lisbon, PT) [dblp]
- Valentin Mayer-Eichberger (Isotronic - Berlin, DE) [dblp]
- Ciaran McCreesh (University of Glasgow, GB)
- Stefan Mengel (CNRS, CRIL - Lens, FR) [dblp]
- Sibylle Möhle (MPI für Informatik - Saarbrücken, DE)
- Jakob Nordström (University of Copenhagen, DK & Lund University, SE) [dblp]
- Andy Oertel (Lund University, SE)
- Sebastian Ordyniak (University of Leeds, GB) [dblp]
- Tomáš Peitl (TU Wien, AT)
- Vaidyanathan Peruvemba Ramaswamy (TU Wien, AT)
- Jussi Rintanen (Aalto University, FI) [dblp]
- Torsten Schaub (Universität Potsdam, DE) [dblp]
- Manfred Scheucher (TU Berlin, DE) [dblp]
- Andre Schidler (TU Wien, AT) [dblp]
- Martina Seidl (Johannes Kepler Universität Linz, AT) [dblp]
- Carsten Sinz (Hochschule Karlsruhe, DE) [dblp]
- Takehide Soh (Kobe University, JP)
- Stefan Szeider (TU Wien, AT) [dblp]
- Guido Tack (Monash University - Clayton, AU) [dblp]
- Hélène Verhaeghe (KU Leuven, BE)
- Hai Xia (TU Wien, AT)
- Emre Yolcu (Carnegie Mellon University - Pittsburgh, US)
- Tianwei Zhang (TU Wien, AT)
- Computational Complexity
- Data Structures and Algorithms
- Logic in Computer Science
- propositional satisfiability
- problem formulation
- lower and upper bounds
- constraint propagation
- symmetry breaking