SAT Encodings and Beyond

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.