Theory and Practice of SAT Solving (Dagstuhl Seminar 15171)

Authors Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, Ryan Williams and all authors of the abstracts in this report

Thumbnail PDF


  • Filesize: 1.13 MB
  • 25 pages

Document Identifiers

Author Details

Armin Biere
Vijay Ganesh
Martin Grohe
Jakob Nordström
Ryan Williams
and all authors of the abstracts in this report

Cite AsGet BibTex

Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams. Theory and Practice of SAT Solving (Dagstuhl Seminar 15171). In Dagstuhl Reports, Volume 5, Issue 4, pp. 98-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


This report documents the program and the outcomes of Dagstuhl Seminar 15171 "Theory and Practice of SAT Solving". The purpose of this workshop was to explore one of the most significant problems in all of computer science, namely that of computing whether formulas in propositional logic are satisfiable or not. This problem is believed to be intractable in general (by the theory of NP-completeness). However, the last two decades have seen dramatic developments in algorithmic techniques, and today so-called SAT solvers are routinely and successfully used to solve large-scale real-world instances in a wide range of application areas. A surprising aspect of this development is that the best current SAT solvers are still to a large extent based on methods from the early 1960s, which can often handle formulas with millions of variables but may also get hopelessly stuck on formulas with just a few hundred variables. The fundamental question of when SAT solvers perform well or badly, and what underlying mathematical properties of the formulas influence SAT solver performance, remains very poorly understood. Another intriguing aspect is that much stronger mathematical methods of reasoning about propositional logic formulas are known today, in particular methods based on algebra and geometry, and these methods would seem to have great potential based on theoretical studies. However, attempts at harnessing the power of such methods have conspicuously failed to deliver any significant improvements in practical performance. This workshop gathered leading researchers in applied and theoretical areas of SAT and computational complexity to stimulate an increased exchange of ideas between these two communities. We see great opportunities for fruitful interplay between theoretical and applied research in this area, and believe that this workshop showed beyond doubt that a more vigorous interaction between the two has potential for major long-term impact in computer science, as well for applications in industry.
  • SAT
  • Boolean SAT solvers
  • SAT solving
  • conflict-driven clause learning
  • Gröbner bases
  • pseudo-Boolean solvers
  • proof complexity
  • computational complexity
  • parameterized complexity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail