- Annette Beyer (for administrative matters)
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. The satisfiability problem, SAT for short, stands at the crossroads of logic, graph theory, computer science, computer engineering and computational physics.
In particular SAT is of central importance in various areas of computer science including algorithmics, verification, planning and hardware design. It can express a wide range of combinatorial problems as well as many real-world ones. Due to its potential practical implications an intensive search has been done on how one could solve SAT problems in an automated fashion. The last decade has seen the development of practically-efficient algorithms for SAT, which can solve huge problems instances.
At the same time SAT is very significant from a theoretical point of view. Since the Cook-Levin's 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. Indeed, as stated by Richard Lipton on his blog Gödel's Lost Letter and P = NP such a proof matters since it would tell us why some computational problems are intrinsically more difficult than others, it would suggest new methods that would yield new insights on the fundamental nature of computation and it would help with goals of security for cryptographers.
During the past two decades, an impressive array of diverse techniques from mathematical fields, such as propositional logic, model theory, Boolean function theory, combinatorics, probability, and statistical physics 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 (with an emphasize on mathematical aspects), 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.
Organization of the Seminar and Activities
The workshop brought together 44 researchers from different areas of computer science and mathematics such as logic, complexity theory, algorithms, and proof complexity with complementary expertise. The participants consisted of both senior and junior researchers, including a number of postdocs and a few advanced graduate students.
Participants were invited to present their work and to communicate state-of-the-art advances. Twenty-five talks of various lengths took place over the five days of the workshop. Introductory and tutorial talks of 60 minutes were scheduled prior to workshop. Most of the remaining slots were filled, mostly with shorter talks, as the workshop commenced. The organizers considered it important to leave ample free time for discussion.
Concluding Remarks and Future Plans
The organizers regard the workshop 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 and stated that this seminar was among the most fruitful Dagstuhl seminars they attended.
Finally, the organizers wish to express their gratitude toward the Scientific Directorate of the Center for its support of this workshop, and hope to establish a series of workshops on SAT Interactions in the future.
- Olaf Beyersdorff (University of Leeds, GB) [dblp]
- Uwe Bubeck (Universität Paderborn, DE)
- Catarina Alexandra Carvalho (University of Hertfordshire, GB) [dblp]
- Nadia Creignou (University of Marseille, FR) [dblp]
- Stefan Dantchev (Durham University, GB) [dblp]
- Evgeny Dantsin (Roosevelt University - Chicago, US)
- Anuj Dawar (University of Cambridge, GB) [dblp]
- Arnaud Durand (University Paris-Diderot, FR) [dblp]
- Johannes Ebbing (Leibniz Universität Hannover, DE) [dblp]
- Uwe Egly (TU Wien, AT) [dblp]
- John Franco (University of Cincinnati, US) [dblp]
- Nicola Galesi (Sapienza University of Rome, IT) [dblp]
- Heidi Gebauer (ETH Zürich, CH) [dblp]
- Andreas Goerdt (TU Chemnitz, DE) [dblp]
- Miki Hermann (Ecole Polytechnique - Palaiseau, FR) [dblp]
- Timon Hertli (ETH Zürich, CH) [dblp]
- Edward A. Hirsch (Steklov Institute - St. Petersburg, RU) [dblp]
- Kazuo Iwama (Kyoto University, JP) [dblp]
- Jan Johannsen (LMU München, DE) [dblp]
- Lefteris M. Kirousis (University of Athens, GR & Computer Technology Institute and Press "Eudoxus", GR) [dblp]
- Hans Kleine Büning (Universität Paderborn, DE) [dblp]
- Donald Ervin Knuth (Stanford University, US)
- Juha Kontinen (University of Helsinki, FI) [dblp]
- Alexander S. Kulikov (Steklov Institute - St. Petersburg, RU) [dblp]
- Oliver Kullmann (Swansea University, GB) [dblp]
- Massimo Lauria (KTH Royal Institute of Technology, SE) [dblp]
- Victor W. Marek (University of Kentucky - Lexington, US)
- Barnaby Martin (Middlesex University - London, GB) [dblp]
- Arne Meier (Leibniz Universität Hannover, DE) [dblp]
- Julian-Steffen Müller (Leibniz Universität Hannover, DE)
- Jakob Nordström (KTH Royal Institute of Technology, SE) [dblp]
- Ramamohan Paturi (University of California - San Diego, US) [dblp]
- Rahul Santhanam (University of Edinburgh, GB) [dblp]
- Dominik Alban Scheder (Aarhus University, DK) [dblp]
- Henning Schnoor (Universität Kiel, DE) [dblp]
- Uwe Schöning (Universität Ulm, DE) [dblp]
- Martina Seidl (Universität Linz, AT) [dblp]
- Robert H. Sloan (University of Illinois - Chicago, US) [dblp]
- Ewald Speckenmeyer (Universität Köln, DE) [dblp]
- Stefan Szeider (TU Wien, AT) [dblp]
- Jacobo Torán (Universität Ulm, DE) [dblp]
- Heribert Vollmer (Leibniz Universität Hannover, DE) [dblp]
- Sean Weaver (University of Cincinnati, US) [dblp]
- Xishun Zhao (Sun Yat-sen University - Guangzhou, CN) [dblp]
- data structures / algorithms / complexity / random structures / combinatorics
- satisfiability problem
- computational complexity
- P-NP question
- proof complexity
- phase transition
- quantified Boolean formulas