Knowledge Compilation Using Theory Prime Implicates

Abstract

In this paper, we are mainly concerned with logical compilations of propositional knowledge bases. We propose a new approach to equivalence-preserving knowledge compilation based on a generalization of the standard notion of prime implicate, the theory prime implicates. Our approach consists in taking advantage of tractable theories Φ implied by the knowledge base Σ to make Σ local by computing the theory prime implicates of Σ w.r.t. Φ. As a main result, query answering from theory prime implicates compilations can be done in time polynomial in their sizes. While there is no guarantee that the size of a compilation is not exponentially greater than the size of the original knowledge base, we show that it is smaller than the size of the prime implicates compilation in the general case and it can even be exponentially smaller. Additionally, we present some experimental results providing evidence for the substantial space savings achievable with our compilation technique.