| abstract: | The development of universal reasoning engines has been a main objective of AI since its very early days. The vision here is to relieve system developers from having to worry about reasoning algorithms, focusing only on capturing the necessary knowledge, while delegating algorithmic considerations to these engines. Few decades after this original vision was first conceived, the field of AI is starting to bear its fruits, initially through SAT solvers, and more recently through knowledge compilers (and related model counters).
In this talk, I will discuss some of the progress in realizing this vision, highlighting both successes and missed opportunities. For example, on the satisfiability front, I will present a semantics for modern SAT solvers, which is somewhat distant from how these solvers are commonly understood. I will argue that the lack of this and similar semantics could be the reason behind the lack of recent leaps in SAT solving, which have been sought since the zchaff solver was introduced many years ago. On the knowledge compilation front, I will review some of the key advancements, especially in relation to SAT solving and model counting, and point to some of the major gaps between what the theory says is possible and what current practice allows. I will argue that bridging this gap requires some novelties, especially in how systematic search is currently practiced. I will also discuss some recent breakthroughs that seem to have brought us closer to bridging this gap. |