https://www.dagstuhl.de/20061

February 2 – 7 , 2020, Dagstuhl Seminar 20061

SAT and Interactions

Organizers

Olaf Beyersdorff (Universität Jena, DE)
Uwe Egly (TU Wien, AT)
Meena Mahajan (Institute of Mathematical Sciences – Chennai, IN)
Claudia Nalon (University of Brasilia, BR)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 10, Issue 2 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl's Impact: Documents available
Dagstuhl Seminar Schedule [pdf]

Summary

The problem of deciding whether a propositional formula is satisfiable (SAT) is one of the most fundamental problems in computer science, both theoretically and practically. Its theoretical significance derives from the Cook-Levin Theorem, identifying SAT as the first NP-complete problem. Since then SAT has become a reference for an enormous variety of complexity statements, among them the celebrated Pe vs NP problem: one of seven million-dollar Clay Millennium Problems. Due to its NP hardness, SAT has been classically perceived as an intractable problem, and indeed, unless Pe=NP, no polynomial-time algorithm for SAT exists.

There are many generalisations of the SAT problem to further logics, including quantified Boolean formulas (QBFs) and modal and temporal logics. These logics present even harder satisfiability problems as they are associated with complexity classes such as PSPACE, which encompasses NP. However, QBFs, modal and temporal logics can express many practically relevant problems far more succinctly, thus applying to more real-world problems from artificial intelligence, bioinformatics, verification, and planning.

Due to its practical implications, intensive research has been performed on how to solve SAT problems in an automated fashion. The last decade has seen the development of practically efficient algorithms for SAT, QBFs and further logics and their implementation as solvers, which successfully solve huge industrial instances.

Very often, these developments take place within different communities, e.g., there has been almost no interaction between the areas of SAT/QBF solving and solving for modal logics.

The main aim of the proposed Dagstuhl Seminar therefore was to bring together researchers from proof complexity and proof theory, SAT, MaxSAT and QBF solving, and modal logics so that they can communicate state-of-the-art advances and embark on a systematic interaction that will enhance the synergy between the different areas. As such the seminar was the first workshop (in Dagstuhl and elsewhere) to unite researchers working on both theory and practice of propositional SAT, QBF, and modal logics. One of the specific aims was to foster more interaction between these different communities with the goal to transfer the success of theoretical research on SAT to further logics and SAT problems.

To facilitate such interactions, the seminar included a number of survey talks to introduce neighbouring communities to the main notions, results, and challenges of the represented areas. The following survey talks were given during the seminar:

  • Lutz Straßburger: Introduction to Deep Inference,
  • Vijay Ganesh: Machine Learning and Logic Solvers: The Next Frontier,
  • MikolᚠJanota: QBF Solving and Calculi: An Overview,
  • João Marques-Silva: Practical MaxSAT Solving: A Survey,
  • Cláudia Nalon: Modal Logics: An Overview.

Each of these surveys was accompanied by one or more sessions with contributed talks dedicated to recent specific results of the field.

The seminar also included an open discussion session on `Future Directions of Research', where ideas for a closer interaction between theoretical fields such as proof theory and proof complexity and practical fields such as SAT/QBF and modal solving were discussed.

The organisers believe that the seminar fulfilled their original high goals: most talks were a great success and many participants reported about the inspiring seminar atmosphere, fruitful interactions, and a generally positive experience. The organisers and participants wish to thank the staff and the management of Schloss Dagstuhl for their assistance and excellent support in the arrangement of a very successful and productive event.

Summary text license
  Creative Commons BY 3.0 Unported license
  Olaf Beyersdorff, Uwe Egly, Meena Mahajan, and Claudia Nalon

Dagstuhl Seminar Series

Classification

  • Data Structures / Algorithms / Complexity

Keywords

  • Satisfiability problems
  • Computational and proof complexity
  • Combinatorics
  • Solvers for satisfiability problems
  • Non-classical logics

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.