Dagstuhl Seminar 09461
Algorithms and Applications for Next Generation SAT Solvers
( Nov 08 – Nov 13, 2009 )
Permalink
Organizers
- Bernd Becker (Universität Freiburg, DE)
- Valeria Bertacco (Univ. of Michigan - Ann Arbor, US)
- Rolf Drechsler (Universität Bremen, DE)
- Masahiro Fujita (University of Tokyo, JP)
Contact
- Annette Beyer (for administrative matters)
In the last decade solvers for Boolean satisfiability (SAT solver) have successfully been applied in many different areas such as design automation, databases, artificial intelligence, etc. A major reason triggering this widespread adoption was the development of several sophisticated SAT techniques and as a result, today SAT solvers are the core solving engine behind many industrial and university tools as well.
However, common SAT solvers operate at the Boolean level and, in general, can only solve a satisfiability problem for formulas expressed in propositional logic. Due to the increasing complexity of the considered problems (e.g. exponential growth of the design sizes in circuit verification), in the last years several approaches have been studied which lift the solving engine to higher levels of abstractions and/or logics that have additional representational power, such as quantified Boolean logic or word level descriptions.
Thus, a new generation of SAT solvers - namely Quantified Boolean Formula (QBF) solvers, word-level solvers and SAT Modulo Theories (SMT) solvers - have been introduced. Furthermore, due to the development of multi-core processors, research in the area of (thread-)parallel SAT solving is growing and will be increasingly important in the near future.
The seminar brought together 36 experts from both 'worlds', i.e. researchers investigating new algorithms for solving SAT instances and researchers using SAT for solving problems in a range of application domains, with a particular focus in VLSI CAD (but not exclusively restricted to this area).
An intensive exchange during the seminar initiated discussions and cooperation among the participants and will hopefully lead to further improvements in the next generation SAT algorithms. Moreover, since most of the new techniques are not yet deployed in applications - even if they are often more competitive in contrast to traditional solving paradigms - the seminar provided an excellent forum to familiarize researchers in this area with the new techniques.
- Erika Abraham (RWTH Aachen, DE) [dblp]
- Bernd Becker (Universität Freiburg, DE) [dblp]
- Armin Biere (Universität Linz, AT) [dblp]
- Rolf Drechsler (Universität Bremen, DE) [dblp]
- Jochen Eisinger (Universität Freiburg, DE)
- Alexander Finder (Universität Bremen, DE)
- Martin Fränzle (Universität Oldenburg, DE) [dblp]
- Hiroshi Fujita (Kyushu University - Fukuoka, JP)
- Masahiro Fujita (University of Tokyo, JP) [dblp]
- Malay K. Ganai (NEC Laboratories America, Inc. - Princeton, US)
- Martin Gogolla (Universität Bremen, DE) [dblp]
- Eugene Goldberg (Northeastern University - Boston, US)
- Daniel Große (Universität Bremen, DE) [dblp]
- Youssef Hamadi (Microsoft Research UK - Cambridge, GB) [dblp]
- Ryuzo Hasegawa (Kyushu University - Fukuoka, JP)
- Thomas Heinz (Robert Bosch GmbH - Schwieberdingen, DE)
- Matti Järvisalo (University of Helsinki, FI) [dblp]
- Stephan Kottler (Universität Tübingen, DE)
- Matthew Lewis (Universität Freiburg, DE)
- Paolo Marin (University of Genova, IT) [dblp]
- Yakau Novikau (OneSpin Solutions - München, DE)
- Florian Pigorsch (Universität Freiburg, DE)
- Sven Reimer (Universität Freiburg, DE) [dblp]
- Lakhdar Sais (CNRS - Lens, FR) [dblp]
- Karem A. Sakallah (University of Michigan - Ann Arbor, US) [dblp]
- Torsten Schaub (Universität Potsdam, DE) [dblp]
- Christoph Scholl (Universität Freiburg, DE) [dblp]
- Tobias Schubert (Universität Freiburg, DE) [dblp]
- Martina Seidl (TU Wien, AT) [dblp]
- Laurent Simon (University of Paris South XI, FR) [dblp]
- Carsten Sinz (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Ofer Strichman (Technion - Haifa, IL) [dblp]
- Olga Tveretina (KIT - Karlsruher Institut für Technologie, DE)
- Markus Wedler (TU Kaiserslautern, DE)
- Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
- Robert Wille (Universität Bremen, DE) [dblp]
Classification
- data structures / algorithms / complexity
- hardware
- verification / logic
Keywords
- Boolean Satisfiability
- Formal Methods
- Word Level
- Quantification
- Multi-threading