08. – 13. November 2009, Dagstuhl Seminar 09461
Algorithms and Applications for Next Generation SAT Solvers
Auskunft zu diesem Dagstuhl Seminar erteilt
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.
- Data Structures / Algorithms / Complexity
- Verification / Logic
- Boolean Satisfiability
- Formal Methods
- Word Level