https://www.dagstuhl.de/20371

September 6 – 11 , 2020, Dagstuhl Seminar 20371

Theory and Practice of SAT Solving

Organizers

Olaf Beyersdorff (Universität Jena, DE)
Armin Biere (Johannes Kepler Universität Linz, AT)
Vijay Ganesh (University of Waterloo, CA)
Jakob Nordström (KTH Royal Institute of Technology – Stockholm, SE)

For support, please contact

Annette Beyer for administrative matters

Shida Kunz for scientific matters

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.

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

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support