Ordered Functional Decision Diagrams

Several BDD variants were designed to exploit special features of Boolean functions to achieve better compression rates.Deciding a priori which variant to use is as hard as constructing the diagrams themselves and the conversion between variants comes in general with a prohibitive cost.This observation leads naturally to a growing interest into when and how one can combine existing variants to benefit from their respective sweet spots. In this paper, we introduce a novel framework, termed $\lambda$ Decision Diagram ($\lambda$DD), that revisits BDD from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like ChainDD and ESRBDD, as implementations of a special class of ordered models.We enumerate, in a principled way, all the models of this class and isolate its most expressive model. This new model, termed $\lambda$DD-O-NUCX, is suitable for both dense and sparse Boolean functions, and, unlike ChainDD and ESRBDD, is invariant by negation. The canonicity of $\lambda$DD-O-NUCX is formally verified using the Coq proof assistant. We furthermore provide experimental evidence corroborating our theoretical findings: more expressive $\lambda$DD models achieve, indeed, better memory compression rates.