TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 16381

SAT and Interactions

( 18. Sep – 23. Sep, 2016 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/16381

Organisatoren

Kontakt



Programm

Motivation

Propositional satisfiability (or Boolean satisfiability) is the problem of determining whether the variables of a Boolean formula can be assigned truth values in such a way as to make the formula true. This satisfiability problem, SAT for short, stands at the crossroads of logic, graph theory, computer science, computer engineering and computational physics. Unsurprisingly SAT is of central importance in various areas of computer science including algorithmics, verification, planning, hardware design and artificial intelligence. It can express a wide range of combinatorial problems as well as many real-world ones.

SAT is very significant from a theoretical point of view. Since the Cook-Levin theorem, which has identified SAT as the first NP-complete problem, it has become a reference for an enormous variety of complexity statements. The most prominent one is the question “is P equal to NP?” Proving that SAT is not in P would answer this question negatively. Restrictions and generalizations of the propositional satisfiability problem play a similar rôle in the examination of other complexity classes and relations among them. In particular quantified versions of SAT, QSAT (in which Boolean variables are universally or existentially quantified), as well as variants of SAT in which some notion of minimality is involved, provide prototypical complete problems for every level of the polynomial hierarchy.

During the past three decades, an impressive array of diverse techniques from mathematical fields, such as propositional and first-order logic, model theory, Boolean function theory, complexity, combinatorics and probability has contributed to a better understanding of the SAT problem. Although significant progress has been made on several fronts, most of the central questions remain unsolved so far.

One of the main aims of the seminar is to bring together researchers from different areas of activity who are not only interested in the classical satisfiability problem, but in variations and extensions of it. The goal is that they communicate state-of-the-art advances and embark on a systematic interaction that will enhance the synergy between the different areas. Variations and extensions of SAT include varying the computational goals, considering other propositional logics and extending the problem to formulas with Boolean quantifiers. Computational complexity and proof complexity are then two topics from which one can expect cross-fertilization during this seminar.


Summary

Brief Introduction to the Topic

Propositional satisfiability (or Boolean satisfiability) is the problem of determining whether the variables of a Boolean formula can be assigned truth values in such a way as to make the formula true. This satisfiability problem, SAT for short, stands at the crossroads of logic, graph theory, computer science, computer engineering and computational physics. Indeed, many problems originating from one of these fields typically have multiple translations to satisfiability. Unsurprisingly, SAT is of central importance in various areas of computer science including algorithmics, verification, planning, hardware design and artificial intelligence. It can express a wide range of combinatorial problems as well as many real-world ones.

SAT is very significant from a theoretical point of view. Since the Cook-Levin theorem, which identified SAT as the first NP-complete problem, it has become a reference for an enormous variety of complexity statements. The most prominent one is the question "is P equal to NP?" Proving that SAT is not in P would answer this question negatively. Restrictions and generalizations of the propositional satisfiability problem play a similar rôle in the examination of other complexity classes and relations among them. In particular, quantified versions of SAT (QSAT, in which Boolean variables are universally or existentially quantified) as well as variants of SAT in which some notion of minimality is involved, provide prototypical complete problems for every level of the polynomial hierarchy.

During the past three decades, an impressive array of diverse techniques from mathematical fields, such as propositional and first-order logic, model theory, Boolean function theory, complexity, combinatorics and probability, has contributed to a better understanding of the SAT problem. Although significant progress has been made on several fronts, most of the central questions remain unsolved so far.

One of the main aims of the Dagstuhl seminar was to bring together researchers from different areas of activity in SAT 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.

Concluding Remarks and Future Plans

The organizers regard the seminar as a great success. Bringing together researchers from different areas of theoretical computer science fostered valuable interactions and led to fruitful discussions. Feedback from the participants was very positive as well. Many attendants expressed their wish for a continuation.

Finally, the organizers wish to express their gratitude toward the Scientific Directorate of the Center for its support of this seminar, and hope to be able to continue this series of seminars on SAT and Interactions in the future.

Copyright Olaf Beyersdorff, Nadia Creignou, Uwe Egly, and Heribert Vollmer

Teilnehmer
  • Olaf Beyersdorff (University of Leeds, GB) [dblp]
  • Joshua Lewis Blinkhorn (University of Leeds, GB) [dblp]
  • Ilario Bonacina (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
  • Samuel R. Buss (University of California - San Diego, US) [dblp]
  • Florent Capelli (University Paris-Diderot, FR) [dblp]
  • Leroy Nicholas Chew (University of Leeds, GB) [dblp]
  • Nadia Creignou (Aix-Marseille University, FR) [dblp]
  • Arnaud Durand (University Paris-Diderot, FR) [dblp]
  • Uwe Egly (TU Wien, AT) [dblp]
  • Shiguang Feng (Universität Leipzig, DE) [dblp]
  • John Franco (University of Cincinnati, US) [dblp]
  • Nicola Galesi (Sapienza University of Rome, IT) [dblp]
  • Anselm Haak (Leibniz Universität Hannover, DE) [dblp]
  • Miki Hermann (Ecole Polytechnique - Palaiseau, FR) [dblp]
  • Marijn J. H. Heule (University of Texas - Austin, US) [dblp]
  • Edward A. Hirsch (Steklov Institute - St. Petersburg, RU) [dblp]
  • Kazuo Iwama (Kyoto University, JP) [dblp]
  • Jan Johannsen (LMU München, DE) [dblp]
  • Peter Jonsson (Linköping University, SE) [dblp]
  • Oliver Kullmann (Swansea University, GB) [dblp]
  • Victor Lagerqvist (TU Dresden, DE) [dblp]
  • Florian Lonsing (TU Wien, AT) [dblp]
  • Meena Mahajan (The Institute of Mathematical Sciences, India, IN) [dblp]
  • Barnaby Martin (Durham University, GB) [dblp]
  • Arne Meier (Leibniz Universität Hannover, DE) [dblp]
  • Stefan Mengel (CNRS, CRIL - Lens, FR) [dblp]
  • Jakob Nordström (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
  • Steffen Reith (Hochschule RheinMain, DE) [dblp]
  • Rahul Santhanam (University of Oxford, GB) [dblp]
  • Dominik Alban Scheder (Shanghai Jiao Tong University, CN) [dblp]
  • Irena Schindler (Leibniz Universität Hannover, DE) [dblp]
  • Johannes Schmidt (Jönköping University, SE) [dblp]
  • Uwe Schöning (Universität Ulm, DE) [dblp]
  • Anil Shukla (The Institute of Mathematical Sciences, India, IN) [dblp]
  • Sarah Sigley (University of Leeds, GB)
  • Stefan Szeider (TU Wien, AT) [dblp]
  • Jacobo Torán (Universität Ulm, DE) [dblp]
  • Heribert Vollmer (Leibniz Universität Hannover, DE) [dblp]
  • Christoph M. Wintersteiger (Microsoft Research UK - Cambridge, GB) [dblp]

Verwandte Seminare
  • Dagstuhl-Seminar 12471: SAT Interactions (2012-11-18 - 2012-11-23) (Details)
  • Dagstuhl-Seminar 20061: SAT and Interactions (2020-02-02 - 2020-02-07) (Details)
  • Dagstuhl-Seminar 24421: SAT and Interactions (2024-10-13 - 2024-10-18) (Details)

Klassifikation
  • data structures / algorithms / complexity

Schlagworte
  • satisfiability problems
  • computational complexity
  • proof complexity
  • combinatorics
  • solvers for satisfiability problems
  • reductions to satisfiability problems