DPLL with a trace: from SAT to knowledge compilation

Abstract

We show that the trace of an exhaustive DPLL search can be viewed as a compilation of the propositional theory. With different constraints imposed or lifted on the DPLL algorithm, this compilation will belong to the language of d-DNNF, FBDD, and OBDD, respectively. These languages are decreasingly succinct, yet increasingly tractable, supporting such polynomial-time queries as model counting and equivalence testing. Our contribution is thus twofold. First, we provide a uniform framework, supported by empirical evaluations, for compiling knowledge into various languages of interest. Second, we show that given a particular variant of DPLL, by identifying the language membership of its traces, one gains a fundamental understanding of the intrinsic complexity and computational power of the search algorithm itself. As interesting examples, we unveil the “hidden power” of several recent model counters, point to one of their potential limitations, and identify a key limitation of DPLLbased procedures in general.