Theoretical Foundations of Applied SAT Solving (14w5101)
Albert Atserias (Universitat Politecnica de Catalunya)
Armin Biere (Johannes Kepler University)
Sam Buss (University of California, San Diego)
Antonina Kolokolova (Memorial University of Newfoundland)
Jakob Nordström (KTH Royal Institute of Technology)
Karem Sakallah (University of Michigan)
We believe that a strong case can be made for the importance of an increased exchange between the two fields of SAT solving and proof complexity. While we are not trying to suggest that there have been water-tight partitions between the two areas before, it seems fair to say that the amount of interaction has been low given how many questions would seem to be of mutual interest. Therefore, we see great potential in more developed contacts between proof complexity theorists on the one hand and SAT practitioners on the other, and we believe a BIRS workshop could serve as a powerful stimulus for developments in this direction.
Below, we try to outline some possible areas for discussion during such a workshop. This list is far from exhaustive, and indeed we believe that the workshop as such would help to uncover other new (and perhaps unexpected) questions of common interest.
WHAT MAKES FORMULAS HARD OR EASY IN PRACTICE FOR STATE-OF-THE-ART 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 there is a theoretical complexity measure for formulas than can 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 OTHER 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 DPLL 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 the advent of computers with multi-core processors, 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.
We believe that progress on any of these questions has the potential of influencing the further development of both theoretical and applied research, and to stimulate a further cross-pollination between these two areas.
CAN WE BUILD SAT SOLVERS BASED ON STRONGER PROOF SYSTEMS THAN RESOLUTION?
Although the performance of modern DPLL-based 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 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 strictly 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. We believe it would be fruitful to invite experts on algebraic and geometric SAT solving 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.