Dagstuhl Seminar 23261
SAT Encodings and Beyond
( Jun 25 – Jun 30, 2023 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/23261
Organizers
- Marijn J. H. Heule (Carnegie Mellon University - Pittsburgh, US)
- Inês Lynce (University of Lisbon, PT)
- Stefan Szeider (TU Wien, AT)
- Neng-Fa Zhou (Brooklyn College, US)
Contact
- Michael Gerke (for scientific matters)
- Jutka Gasiorowski (for administrative matters)
Schedule
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 called a SAT encoding. The encoding itself is often the crucial part that determines whether the solver can solve the problem efficiently, making the encoding techniques at least as important as the solving techniques. Hence, much effort has been put into researching efficient encoding techniques.
Other previous scientific meetings primarily focused on solving techniques, not on encodings. Hence, this Dagstuhl Seminar provided an overdue opportunity for an in-depth discussion of the state-of-the-art of encodings and future challenges and research avenues. When planning the seminar, we identified the following five critical topics.
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. Which methods can overcome these limitations?
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 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.
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 is how the encoding part of the toolchain 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. These more general problems require new encoding techniques.
We invited key researchers to cover these topics and were happy that most of the people we wished for accepted the invitation. Hence, we could approach participants individually to solicit longer survey talks to cover these topics by top experts. Shorter, focused talks complemented these longer survey-like talks. The talks covered various encoding aspects for particular solving paradigms, including SAT, CP, ASP, MaxSAT, and QBF.
We were delighted to have the industrial perspective covered by Andreas Falkner (Siemens AG), who presented challenges in industrial product configuration.
Other talks were devoted to symmetry-breaking techniques that boost SAT-based combinatorial search, which included a live demo of the SMS tool; another focus of several talks was the verification of results obtained via encodings. Some talks explored the theoretical limits of encodings and the connection between computer algebra systems and SAT encodings.
In addition to the talks, we had an open-problems and challenges session and dedicated time for group work. The posed problems asked for desirable properties for proof logging, how encodings can ensure that propagation on a high level implies propagation on a low level, how encodings for enumeration and counting can be established, how one can measure the usefulness of auxiliary variables in encodings, how to verify that an encoding is correct, and the exact computational complexity of minimal resolution proof length (in binary). Also, efficient encodings for several concrete problems were posed, including Golumb Rulers, the Connect-4 game, the metric dimension of hypercubes, the independent configuration problem, problems related to Steiner Triples, line arrangements with a limited number of triangles, and block designs that appear in product configuration. We formed working groups to tackle some of these problems and had a brief session where progress on these problems was reported and discussed.
Overall, we are pleased with the outcome of the seminar. We have met our objectives and started a highly stimulating discussion and exchange of ideas, covering the state of the art and future challenges. Still, it also became clear that encodings are a far-reaching topic that leaves many challenging open questions for future work. So, a follow-up Dagstuhl Seminar in the future is strongly indicated.
Creative Commons BY 4.0
Marijn J. H. Heule, Inês Lynce, and Stefan Szeider
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.
Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Neng-Fa Zhou
- 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) [dblp]
- 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) [dblp]
- 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)
Classification
- Computational Complexity
- Data Structures and Algorithms
- Logic in Computer Science
Keywords
- propositional satisfiability
- problem formulation
- lower and upper bounds
- constraint propagation
- symmetry breaking
