TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


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

Contact

Shared Documents


Schedule

Summary

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.

Copyright Marijn J. H. Heule, Inês Lynce, and Stefan Szeider

Motivation

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.
Copyright Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Neng-Fa Zhou

Participants

Classification
  • Computational Complexity
  • Data Structures and Algorithms
  • Logic in Computer Science

Keywords
  • propositional satisfiability
  • problem formulation
  • lower and upper bounds
  • constraint propagation
  • symmetry breaking