25. – 30. Juni 2023, Dagstuhl-Seminar 23261

SAT Encodings and Beyond


Marijn J. H. Heule (Carnegie Mellon University – Pittsburgh, US)
Inês Lynce (Technical University of Lisboa, PT)
Stefan Szeider (TU Wien, AT)
Neng-Fa Zhou (Brooklyn College, US)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Jutka Gasiorowski zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen


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.

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.

Motivation text license
  Creative Commons BY 4.0
  Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Neng-Fa Zhou


  • Computational Complexity
  • Data Structures And Algorithms
  • Logic In Computer Science


  • Propositional satisfiability
  • Problem formulation
  • Lower and upper bounds
  • Constraint propagation
  • Symmetry breaking


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.