19.04.15 - 24.04.15, Seminar 15171

Theory and Practice of SAT Solving

The following text appeared on our web pages prior to the seminar, and was included as part of the invitation.

Motivation

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.