The purpose of this Dagstuhl Seminar is to explore one of the most significant problems in all of computer science, namely that of deciding satisfiability of logic formulas, or SAT. This is a problem of immense importance both theoretically and practically. On the one hand, it is believed to be intractable in the worst case, and deciding whether this is so is one of the famous million-dollar Clay Millennium Problems (the P vs. NP problem). On the other hand, today so-called SAT solvers are routinely used to solve large-scale real-world instances in a wide range of application areas.

During the last two decades, there have been dramatic – and surprising – developments in SAT solving technology that have improved real-world performance by many orders of magnitude. But perhaps even more surprisingly, the best solvers today are still based on relatively simple methods from the early 1960s (albeit with many clever optimizations), searching for proofs in the so-called resolution proof system. While such solvers can often handle formulas with millions of variables, there are also tiny formulas with just a few hundred variables for which even the very best solvers get hopelessly stuck. The fundamental questions of when SAT solvers perform well or badly, and what properties of the formulas influence SAT solver performance, remain very poorly understood. Other practical SAT solving issues, such as how to optimize memory management and how to exploit parallelization on modern multicore architectures, are even less well studied and understood from a theoretical point of view.

On the theoretical side, many methods of reasoning about logic formulas have been studied, e.g., based on algebra and geometry, and have been shown to be exponentially stronger than resolution. Intriguingly, however, so far, most attempts to harness the power of such methods have failed to deliver any significant improvements in practical performance. And while resolution is a reasonably well-understood proof system, even very basic questions about these stronger algebraic and geometric methods remain wide open.

The goal of this seminar is to gather leading researchers in applied and theoretical areas surrounding SAT, and to stimulate an increased exchange of ideas between these communities. We believe that theoretical research can shed light on the power and limitations of current and possible future SAT solving techniques, and that problems encountered in applied SAT solving can give rise to interesting new areas in theoretical research. We also see great potential for technology transfer between SAT and neighboring areas such as SMT solving, QBF solving, constraint programming, and mixed integer linear programming. It is our hope that this seminar will serve as a platform to stimulate more vigorous interaction between practitioners and theoreticians, spawning further progress which could have major long-term impact in both academia and industry.

Creative Commons BY 3.0 DE

Olaf Beyersdorff, Armin Biere, Vijay Ganesh, and Jakob Nordström