Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 09461

Algorithms and Applications for Next Generation SAT Solvers

( Nov 08 – Nov 13, 2009 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:




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]

  • data structures / algorithms / complexity
  • hardware
  • verification / logic

  • Boolean Satisfiability
  • Formal Methods
  • Word Level
  • Quantification
  • Multi-threading