Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation

Abstract

Satisfiability testing has seen significant growth over the last decade, leading to orders of magnitude improvements in performance over a relatively short period of time. State of the art algorithms for satisfiability, which are based on DPLL search, were originally meant to find a single satisfying assignment, but their scope has been extended recently to perform exhaustive searches for the purpose of counting and enumerating models. Moreover, the algorithms have been augmented with sophisticated techniques, such as component analysis and formula caching, which are critical to their performance in real-world applications. In a parallel thread of developments, work has been commencing in the area of knowledge compilation, which aims at converting knowledge bases into tractable representations that allow some hard operations to be performed in polytime on the compiled representations. Work in this area has lead to the identification of a comprehensive taxonomy of tractable languages that explicates their relative succinctness and the polytime operations they support.