On OBDDs for CNFs of Bounded Treewidth

ABSTRACT. Knowledge compilation is a rewriting approach to propositional knowledge representation. The `knowledge base' is initially represented as a CNF for which many important types of queries are NP-complete to answer. Therefore, the CNF is compiled into another representation for which the minimal requirement is that the clause entailment query (can the given partial assignment be extended to a complete satisfying assignment?) can be answered in a polynomial time. Such transformation can result in exponential blow up of the representation size. A possible way to circumvent this issue is to identify a structural parameter of the input CNF such that the resulting transformation is exponential in this parameter and polynomial in the number of variables. A notable result in this direction is an $O(2^kn)$ upper bound on the size of Decomposable Negation Normal Form (DNNF) proposed by (Darwiche, JACM 2001), where $n$ is the number of variables of the given CNF and $k$ is the treewidth of its primal graph. Quite recently this upper bound has been shown to hold for Sentential Decision Diagrams (Darwiche, IJCAI2011), a subclass of DNNF that can be considered as a generalization of the famous Ordered Binary Decision Diagrams (OBDD) and shares with the OBDD the key nice features (e.g. poly-time equivalence testing). Under this parameterization, the best known upper bound for an OBDD is $O(n^k)$ (Ferrara, Pan, Vardi; LPAR2005). A natural question is whether a fixed parameter upper bound holds for OBDD.

In this paper we answer this question negatively. In particular, we demonstrate an infinite class of CNFs of the primal graph treewidth at most $k$ for which the OBDD size is at least $O(n^{k/4})/o(n)$ thus providing a separation from SDD and essentially matching the upper bound of Ferrara, Pan, and Vardi. We also establish a more optimistic version of the $O(n^k)$ upper bound for the OBDD showing that it in fact holds when $k$ is the treewidth of the incidence graph of the given CNF and thus applies for `sparse' CNFs with large clauses.