http://www.dagstuhl.de/09461

November 8 – 13 , 2009, Dagstuhl Seminar 09461

Algorithms and Applications for Next Generation SAT Solvers

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)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Seminar Proceedings DROPS
List of Participants

Summary

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.

Classification

  • Data Structures / Algorithms / Complexity
  • Hardware
  • Verification / Logic

Keywords

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

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support