https://www.dagstuhl.de/20371

06. – 11. September 2020, Dagstuhl-Seminar 20371

CANCELLED Theory and Practice of SAT Solving

Due to the Covid-19 pandemic, this seminar was cancelled.

Organisatoren

Olaf Beyersdorff (Universität Jena, DE)
Armin Biere (Johannes Kepler Universität Linz, AT)
Vijay Ganesh (University of Waterloo, CA)
Jakob Nordström (University of Copenhagen, DK & Lund University, SE)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Annette Beyer zu administrativen Fragen

Shida Kunz zu wissenschaftlichen Fragen

Motivation

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.

Motivation text license
  Creative Commons BY 3.0 DE
  Olaf Beyersdorff, Armin Biere, Vijay Ganesh, and Jakob Nordström

Related Dagstuhl-Seminar

Classification

  • Data Structures / Algorithms / Complexity
  • Optimization / Scheduling
  • Verification / Logic

Keywords

  • Boolean satisfiability
  • SAT solving
  • Computational complexity
  • Proof complexity
  • Combinatorial optimization

Dokumentation

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).

Publikationen

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

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.