| abstract: | I discuss in this talk two influential areas of automated reasoning, satisfiability and knowledge compilation. Historically, these two areas have been developing independently, but have come to an intersection point recently that is interesting both theoretically and practically. In particular, I will show that the intersection point rests on recent extensions of satisfiability solvers to perform exhaustive searches for the purpose of model counting and enumeration, aided by sophisticated techniques such as component analysis and formula caching. More precisely, I will show that the traces of these exhaustive search algorithms can be interpreted as sentences and that each search algorithm corresponds to a (tractable) language generated by all its possible executions. I will provide multiple matches between key search algorithms and well known tractable languages and discuss two implications of this matching: (1) harnessing advances in satisfiability to compile knowledge bases, leading to some new algorithms for knowledge compilation, and (2) invoking known results on tractable languages to identify previously unknown powers and limitations of search algorithms. The talk will provide ample empirical results and applications from various areas, including planning, diagnosis and probabilistic reasoning.
|