Keynote Speakers
| Erich Grädel | The State of the Art in the Quest for a Logic for Polynomial Time |
| The problem whether there is a logic that precisely captures polynomial time on all finite structures is the fundamental problem of finite model theory and descriptive complexity. It goes back to the 1980s and is also a problem that Helmut Veith has been very much interested in. I shall discuss the state of the art and the perspectives of current research concerning this problem. The logic of reference on this area is fixed-point logic with counting (FPC), although it has been known for a long time that ist does not express all polynomial-time properties of finite structures. Currently studied candidates for a logic that might capture PTIME are on one side extensions of FPC by algebraic operators such as the rank of definable matrices, and on the other side Choiceless Polynomial Time (CPT), a logic that is based on the manipulation of hereditarily finite sets over the given input structure. Recent research has revealed new algorithmic problems that are CPT-definable and new classes on which CPT actually captures PTIME. A problem that had been proposed by Rossman as a potential candidate for separating CPT from PTIME is the summation problem for Abelian groups and semigroups. However, we show that that this problem is definable in CPT, and actually even in fixed-point logic with counting. On the other side, a probabilistic argument shows that it is not definable in CPT without counting, not even for Abelian groups. | |
| Moshe Vardi | The Automated-Reasoning Revolution: From Theory to Practice and Back |
|
For the past 40 years computer scientists generally believed that NP-complete problems are intractable. In particular, Boolean satisfiability (SAT), as a paradigmatic automated-reasoning problem, has been considered to be intractable. Over the past 20 years, however, there has been a quiet, but dramatic, revolution, and very large SAT instances are now being solved routinely as part of software and hardware design. In this talk I will review this amazing development and show how automated reasoning is now an industrial reality. I will then describe how we can leverage SAT solving to accomplish other automated-reasoning tasks. Counting the the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with applications in software testing, software synthesis, machine learning, personalized learning, and more. While the theory of these problems has been thoroughly investigated since the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances. Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and Satisfiability Modulo Theory, that scales to formulas with hundreds of thousands of variables without giving up correctness guarantees. The talk is accesible to a general CS audience. |