Dagstuhl Seminar 20061
SAT and Interactions
( Feb 02 – Feb 07, 2020 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/20061
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)
Contact
- Michael Gerke (for scientific matters)
- Annette Beyer (for administrative matters)
Impacts
- MaxSAT resolution and subcube sums : article in 23nd International Conference on Theory and Applications of Satisfiability Testing (SAT’20) - Filmus, Yuval; Mahajan, Meena - Toronto : University, 2020. - 18 pp..
- Modal logic and the polynomial hierarchy - Das, Anupam; Marin, Sonia - London : College Publications, 2022. - pp. 329-348 - (Advances in Modal Logic ; 14 : article).
Schedule
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 P vs NP problem: one of seven milliondollar Clay Millennium Problems. Due to its NP hardness, SAT has been classically perceived as an intractable problem, and indeed, unless P=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.
The main aim of this Dagstuhl Seminar is to bring together researchers from different areas of activity in SAT, including computational and proof complexity, SAT and QBF solving, and modal, temporal and further nonclassical 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.
Creative Commons BY 3.0 DE
Olaf Beyersdorff, Uwe Egly, Meena Mahajan, and Claudia Nalon
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:
- Massimo Lauria: Proof Complexity: A Survey,
- 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.
Olaf Beyersdorff, Uwe Egly, Meena Mahajan, and Claudia Nalon
- Olaf Beyersdorff (Universität Jena, DE) [dblp]
- Joshua Lewis Blinkhorn (Universität Jena, DE) [dblp]
- Benjamin Böhm (Universität Jena, DE)
- Ilario Bonacina (UPC Barcelona Tech, ES) [dblp]
- Florent Capelli (Lille I University, FR) [dblp]
- Leroy Nicholas Chew (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Judith Clymo (University of Leeds, GB)
- Nadia Creignou (Aix-Marseille University, FR) [dblp]
- Anupam Das (University of Birmingham, GB) [dblp]
- Susanna de Rezende (The Czech Academy of Sciences - Prague, CZ) [dblp]
- Akhil Dixit (University of California - Santa Cruz, US)
- Clare Dixon (University of Liverpool, GB) [dblp]
- Uwe Egly (TU Wien, AT) [dblp]
- Vijay Ganesh (University of Waterloo, CA) [dblp]
- Azza Gaysin (Charles University - Prague, CZ)
- Edward A. Hirsch (Steklov Institute - St. Petersburg, RU) [dblp]
- Ullrich Hustadt (University of Liverpool, GB) [dblp]
- Mikoláš Janota (IST - Lisbon, PT) [dblp]
- Jan Johannsen (LMU München, DE) [dblp]
- Hans Kleine Büning (Universität Paderborn, DE) [dblp]
- Oliver Kullmann (Swansea University, GB) [dblp]
- Massimo Lauria (Sapienza University of Rome, IT) [dblp]
- Meena Mahajan (Institute of Mathematical Sciences - Chennai, IN) [dblp]
- Joao Marques-Silva (University of Toulouse, FR) [dblp]
- Barnaby Martin (Durham University, GB) [dblp]
- Stefan Mengel (CNRS, CRIL - Lens, FR) [dblp]
- Claudia Nalon (University of Brasilia, BR) [dblp]
- Jakob Nordström (University of Copenhagen, DK & Lund University, SE) [dblp]
- Dirk Pattinson (Australian National University - Canberra, AU) [dblp]
- Tomáš Peitl (Universität Jena, DE) [dblp]
- Renate Schmidt (University of Manchester, GB) [dblp]
- Uwe Schöning (Universität Ulm, DE) [dblp]
- David R. Sherratt (Universität Jena, DE)
- Anil Shukla (Indian Institute of Technology Ropar - Rupnagar, IN) [dblp]
- Friedrich Slivovsky (TU Wien, AT) [dblp]
- Gaurav Sood (Institute of Mathematical Sciences - Chennai, IN)
- Lutz Straßburger (INRIA Saclay - Île-de-France, FR) [dblp]
- Jacobo Torán (Universität Ulm, DE) [dblp]
- Marc Vinyals (Technion - Haifa, IL) [dblp]
- Florian Wörz (Universität Ulm, DE)
Related Seminars
Classification
- data structures / algorithms / complexity
Keywords
- satisfiability problems
- computational and proof complexity
- combinatorics
- solvers for satisfiability problems
- non-classical logics
