SDDs are Exponentially More Succinct than OBDDs

TL;DR

This paper proves that sentential decision diagrams (SDDs) are exponentially more succinct than ordered binary decision diagrams (OBDDs) for certain boolean functions, establishing a theoretical separation that settles an open problem.

Contribution

The paper demonstrates an exponential size separation between SDDs and OBDDs, providing the first such theoretical proof and improving upon previous quasipolynomial results.

Findings

SDDs can be exponentially more succinct than OBDDs for specific functions.

Constructed a family of boolean functions with polynomial SDD size and exponential OBDD size.

Settled an open problem in knowledge compilation regarding the relative succinctness of SDDs and OBDDs.

Abstract

Introduced by Darwiche (2011), sentential decision diagrams (SDDs) are essentially as tractable as ordered binary decision diagrams (OBDDs), but tend to be more succinct in practice. This makes SDDs a prominent representation language, with many applications in artificial intelligence and knowledge compilation. We prove that SDDs are more succinct than OBDDs also in theory, by constructing a family of boolean functions where each member has polynomial SDD size but exponential OBDD size. This exponential separation improves a quasipolynomial separation recently established by Razgon (2013), and settles an open problem in knowledge compilation.