Dagstuhl-Seminar 15171
Theory and Practice of SAT Solving
( 19. Apr – 24. Apr, 2015 )
(zum Vergrößern in der Bildmitte klicken)
Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:
https://www.dagstuhl.de/15171
Organisatoren
- Armin Biere (Universität Linz, AT)
- Vijay Ganesh (University of Waterloo, CA)
- Martin Grohe (RWTH Aachen, DE)
- Jakob Nordström (KTH Royal Institute of Technology, SE)
- Ryan Williams (Stanford University, US)
Kontakt
- Annette Beyer (für administrative Fragen)
Programm
The purpose of this seminar is to explore one of the most significant problems in all of computer science, namely that of proving logic formulas. This is a problem of immense importance both theoretically and practically. On the one hand, it is believed to be intractable in the worst case, and deciding whether this is so is one of the famous million dollar Clay Millennium Problems (the P vs. NP problem). On the other hand, today so-called SAT solvers are routinely and successfully used to solve large-scale real-world instances in a wide range of application areas (such as hardware and software verification, electronic design automation, artificial intelligence research, cryptography, bioinformatics, operations research, and railway signalling systems, just to name a few examples).
During the last 10-15 years, there have been dramatic --- and surprising --- developments in SAT solving technology that have improved real-world performance by many orders of magnitude. But perhaps even more surprisingly, the best SAT solvers today are still based on relatively simple methods from the early 1960s (albeit with many clever optimizations), searching for proofs in the so-called resolution proof system. While such solvers can often handle formulas with millions of variables, there are also known tiny formulas with just a few hundred variables that cause even the very best solvers to stumble. The fundamental questions of when SAT solvers perform well or badly, and what properties of the formulas influence SAT solver performance, remain very poorly understood. Other practical SAT solving issues, such as how to optimize memory management and how to exploit parallelization on modern multicore architectures, are even less well studied and understood from a theoretical point of view.
On the theoretical side, during the last couple of decades other mathematical methods of reasoning than resolution have been studied and have been shown to be much stronger than resolution, in particular methods based on algebra and geometry. It is an intriguing fact, however, that so far attempts to harness the power of such methods have conspicuously failed to deliver any significant improvements in practical performance. And while resolution is a reasonably well-understood proof system, even very basic questions about these stronger algebraic and geometric methods remain wide open.
The goal of this seminar is to gather leading researchers in applied and theoretical areas of SAT and computational complexity and to stimulate an increased exchange of ideas between these two communities. We believe that computational complexity can shed light on the power and limitations on current and possible future SAT solving techniques, and that problems encountered in SAT solving can give rise to interesting new areas in theoretical research. We see great potential for interdisciplinary research at the border between theory and practice in this area, and believe that this seminar could serve as a platform to stimulate more vigorous interaction between practitioners and theoreticians, spawning further progress which could have major long-term impact in both academia and industry.
This seminar brought together researchers working in the areas of applied SAT solving on the one hand, and in proof complexity and neighbouring areas of computational complexity theory on the other, in order to communicate new ideas, techniques, and analysis from both the practical and theoretical sides.
The goals of this endeavour are to better understand why modern SAT solvers work so efficiently for many large-scale real-world instances, and in the longer term to discover new strategies for SAT solving that could go beyond the present "conflict-driven clause-learning" paradigm and deliver substantial further gains in practical performance.
Topics of the Workshop
This seminar explored one of the most significant problems in all of mathematics and computer science, namely that of proving logic formulas. This is a problem of immense importance both theoretically and practically. On the one hand, it is believed to be intractable in general, and deciding whether this is so is one of the famous million dollar Clay Millennium Problems (the P vs. NP problem). On the other hand, today so-called SAT solvers are routinely and successfully used to solve large-scale real-world instances in a wide range of application areas (such as hardware and software verification, electronic design automation, artificial intelligence research, cryptography, bioinformatics, operations research, and railway signalling systems, just to name a few examples).
During the last 15-20 years, there have been dramatic - and surprising - developments in SAT solving technology that have improved real-world performance by many orders of magnitude. But perhaps even more surprisingly, the best SAT solvers today are still based on relatively simple methods from the early 1960s, searching for proofs in the so-called resolution proof system. While such solvers can often handle formulas with millions of variables, there are also known tiny formulas with just a few hundred variables that cause even the very best solvers to stumble. The fundamental question of when SAT solvers perform well or badly, and what underlying properties of the formulas influence SAT solver performance, remains very poorly understood. Other practical SAT solving issues, such as how to optimize memory management and how to exploit parallelization on modern multicore architectures, are even less well studied and understood from a theoretical point of view.
Another intriguing fact is that although other mathematical methods of reasoning are known that are much stronger than resolution in theory, in particular methods based on algebra and geometry, attempts to harness the power of such methods have failed to deliver any significant improvements in practical performance - indeed, such solvers often struggle even to match the performance of resolution-based solvers. And while resolution is a fairly well-understood proof system, even very basic questions about these stronger algebraic and geometric methods remain wide open.
We believe that computational complexity can shed light on the power and limitations on current and possible future SAT solving techniques, and that problems encountered in SAT solving can spawn interesting new areas in theoretical research. We see great potential for interdisciplinary research at the border between theory and practice in this area, and believe that more vigorous interaction between practitioners and theoreticians could have major long-term impact in both academia and industry.
Goals of the Workshop
A strong case can be made for the importance of increased exchange between the two fields of SAT solving on the one hand and proof complexity (and more broadly computational complexity) on the other. While the two areas have enjoyed some exchanges, it seems fair to say that there has been relatively low level of interaction, given how many questions would seem to be of mutual interest. Below, we try to outline some such questions that served as motivation for organizing this seminar. We want to stress that this list is far from exhaustive, and in fact we believe one important outcome of the seminar was to stimulate the process of uncovering other questions of common interest.
What Makes Formulas Hard or Easy in Practice for Modern SAT Solvers?
The best SAT solvers known today are based on the DPLL procedure, augmented with optimizations such as conflict-driven clause learning (CDCL) and restart strategies. The propositional proof system underlying such algorithms, resolution, is arguably the most well-studied system in all of proof complexity.
Given the progress during the last decade on solving large-scale instances, it is natural to ask what lies behind the spectacular success of CDCL solvers at solving these instances. And given that there are still very small formulas that resist even the most powerful CDCL solvers, a complementary interesting question is if one can determine whether a particular formula is hard or tractable. Somewhat unexpectedly, very little turns out to be known about these questions.
In view of the fundamental nature of the SAT problem, and in view of the wide applicability of modern SAT solvers, this seems like a clear example of a question of great practical importance where the theoretical field of proof complexity could potentially provide useful insights. In particular, one can ask whether one could find theoretical complexity measures for formulas than would capture the practical hardness of these formulas in some nice and clean way. Besides greatly advancing our theoretical understanding, answering such a question could also have applied impact in the longer term by clarifying the limitations, and potential for further improvements, of modern SAT solvers.
Can Proof Complexity Shed Light on Crucial SAT Solving Issues?
Understanding the hardness of proving formulas in practice is not the only problem for which more applied researchers would welcome contributions from theoretical computer scientists. Examples of some other possible practical questions that would merit from a deeper theoretical understanding follow below.
- Firstly, we would like to study the question of memory management. One major concern for clause learning algorithms is to determine how many clauses to keep in memory. Also, once the algorithm runs out of the memory currently available, one needs to determine which clauses to throw away. These questions can have huge implications for performance, but are poorly understood.
- In addition to clause learning, the concept of restarts is known to have decisive impact on the performance on modern CDCL solvers. It would be nice to understand theoretically why this is so. The reason why clause learning increases efficiency greatly is clear -- without it the solver will only generate so-called tree-like proofs, and tree-like resolution is known to be exponentially weaker than general resolution. However, there is still ample room for improvement of our understanding of the role of restarts and what are good restart strategies.
- Given that modern computers are multi-core architectures, a highly topical question is whether this (rather coarse-grained) parallelization can be used to speed up SAT solving. Our impression is that this is an area where much practical work is being carried out, but where comparatively little theoretical study has been done. Thus, the first step here would consist of understanding what are the right questions to ask and coming up with a good theoretical framework for investigating them. While there are some successful attempts in parallelizing SAT, obtained speed-ups are rather modest. This is a barrier for further adoption of SAT technology already today and will be become a more substantial problem as thousands of cores and cloud computing are becoming the dominant computing platforms. A theoretical understanding on how SAT can be parallelized will be essential to develop new parallelization strategies to adapt SAT to this new computing paradigm.
Can we build SAT Solvers based on Stronger Proof Systems than Resolution?
Although the performance of modern CDCL SAT solvers is impressive, it is nevertheless astonishing, not to say disappointing, that the state-of-the-art solvers are still based on simple resolution. Resolution lies very close to the bottom in the hierarchy of propositional proof systems, and there are many other proof systems based on different forms of mathematical reasoning that are known to be strictly stronger. Some of these appear to be natural candidates for serving as a basis for stronger SAT solvers than those using CDCL.
In particular, proof systems such as polynomial calculus (based on algebraic reasoning) and cutting planes (based on geometry) are known to be exponentially more powerful than resolution. While there has been some work on building SAT solvers on top of these proof systems, progress has been fairly limited. As part of the seminar, we invited experts on algebraic and geometric techniques to discuss what the barriers are that stops us from building stronger algebraic or geometric SAT solvers, and what is the potential for future improvements. An important part of this work would seem to be to gain a deeper theoretical understanding of the power and limitations of these proof methods. Here there are a number of fairly long-standing open theoretical questions. At the same time, only in the last couple of years proof complexity has made substantial progress, giving hope that the time is ripe for decisive break-throughs in these areas.
Organization of the Workshop
The scientific program of the seminar consisted of 26 talks. Among these there were five 80-minute tutorials on core topics of the seminar:
- proof complexity (Paul Beame),
- conflict-driven clause learning (CDCL) SAT solvers (João Marques-Silva),
- proof systems connected to SAT solving (Sam Buss),
- preprocessing and inprocessing (Matti Järvisalo),
- SAT and SMT (Nikolaj Bjørner).
Throughout, the tutorials were well-received as a means of introducing the topics and creating a common frame of reference for participants from the different communities.
There were also nine slighly shorter survey talks of 50 minutes which were intended to give overviews of a number of important topics for the seminar:
- semialgebraic proof systems (Albert Atserias),
- pseudo-Boolean constraints and CDCL (Daniel Le Berre),
- Gröbner bases (Manuel Kauers),
- SAT-enabled verification of state transition systems, (Karem Sakallah),
- SAT and computational complexity (Ryan Williams)
- the (strong) exponential time hypothesis and consequences (Ryan Williams),
- SAT and parameterized complexity (Stefan Szeider),
- QBF solving (Nina Narodytska),
- random satisfiability (Dimitris Achlioptas).
Most tutorials and survey talks were scheduled early in the week, to create a conducive atmosphere for collaboration on open problems later in the week. The rest of the talks were 25-minute presentations on recent research of the participants. The time between lunch and afternoon coffee was left for self-organized collaborations and discussions, and there was no schedule on Wednesday afternoon.
Based on polling of participants before the seminar week, it was decided to have an open problem session on Monday evening, and on Wednesday evening there was a panel discussion. The organizing committee also considered the option of having a poster session to give more researchers the opportunity to present recent research results, but the feedback in the participant poll was negative and so this idea was dropped.
Creative Commons BY 3.0 Unported license
Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams
- Erika Abraham (RWTH Aachen, DE) [dblp]
- Dimitris Achlioptas (University of California - Santa Cruz, US) [dblp]
- Albert Atserias (UPC - Barcelona, ES) [dblp]
- Gilles Audemard (CNRS - Lens, FR) [dblp]
- Paul Beame (University of Washington - Seattle, US) [dblp]
- Christoph Berkholz (KTH Royal Institute of Technology, SE) [dblp]
- Olaf Beyersdorff (University of Leeds, GB) [dblp]
- Armin Biere (Universität Linz, AT) [dblp]
- Nikolaj S. Bjørner (Microsoft Corporation - Redmond, US) [dblp]
- Ilario Bonacina (Sapienza University of Rome, IT) [dblp]
- Sam Buss (University of California - San Diego, US) [dblp]
- Amin Coja-Oghlan (Goethe-Universität - Frankfurt a. M., DE) [dblp]
- Jessica Davies (IST Austria - Klosterneuburg, AT) [dblp]
- Holger Dell (Universität des Saarlandes, DE) [dblp]
- Jan Elffers (KTH Royal Institute of Technology, SE) [dblp]
- John Franco (University of Cincinnati, US) [dblp]
- Andreas Fröhlich (Universität Linz, AT) [dblp]
- Vijay Ganesh (University of Waterloo, CA) [dblp]
- Alexandra Goultiaeva (Google Waterloo, CA) [dblp]
- Martin Grohe (RWTH Aachen, DE) [dblp]
- Daniel Große (Universität Bremen, DE) [dblp]
- Edward A. Hirsch (Steklov Institute - St. Petersburg, RU) [dblp]
- Holger H. Hoos (University of British Columbia - Vancouver, CA) [dblp]
- Mikoláš Janota (INESC-ID - Lisboa, PT) [dblp]
- Matti Järvisalo (University of Helsinki, FI) [dblp]
- Manuel Kauers (Universität Linz, AT) [dblp]
- Oliver Kullmann (Swansea University, GB) [dblp]
- Massimo Lauria (KTH Royal Institute of Technology, SE) [dblp]
- Daniel Le Berre (CNRS - Lens, FR) [dblp]
- Sharad Malik (Princeton University, US) [dblp]
- Joao Marques-Silva (INESC-ID - Lisboa, PT) [dblp]
- Nina Narodytska (Carnegie Mellon University, US) [dblp]
- Jakob Nordström (KTH Royal Institute of Technology, SE) [dblp]
- Yakau Novikau (OneSpin Solutions - München, DE)
- Albert Oliveras (UPC - Barcelona, ES) [dblp]
- Pavel Pudlák (Czech Academy of Sciences - Prague, CZ) [dblp]
- Alexander Razborov (University of Chicago, US) [dblp]
- Kristin Yvonne Rozier (University of Cincinnati, US) [dblp]
- Karem A. Sakallah (University of Michigan - Ann Arbor, US) [dblp]
- Martina Seidl (Universität Linz, AT) [dblp]
- Laurent Simon (University of Bordeaux, FR) [dblp]
- Niklas Sörensson (Mentor Graphics - Göteborg, SE) [dblp]
- Stefan Szeider (TU Wien, AT) [dblp]
- Alasdair Urquhart (University of Toronto, CA) [dblp]
- Allen Van Gelder (University of California - Santa Cruz, US) [dblp]
- Marc Vinyals (KTH Royal Institute of Technology, SE) [dblp]
- Magnus Wahlström (Royal Holloway University of London, GB) [dblp]
- Ryan Williams (Stanford University, US) [dblp]
Verwandte Seminare
- Dagstuhl-Seminar 22411: Theory and Practice of SAT and Combinatorial Solving (2022-10-09 - 2022-10-14) (Details)
Klassifikation
- data structures / algorithms / complexity
- semantics / formal methods
- verification / logic
Schlagworte
- SAT
- Boolean SAT solvers
- SAT solving
- conflict-driven clause learning
- Groebner bases
- pseudo-Boolean solvers
- proof complexity
- computational complexity
- parameterized complexity
