Ordered Functional Decision Diagrams: A Functional Semantics For Binary Decision Diagrams
This work provides a foundational classification for BDD variants, aiding researchers and practitioners in automated reasoning and verification, though it is incremental as it builds on existing BDD theory.
The paper tackles the problem of classifying and extending Binary Decision Diagrams (BDDs) by introducing a functional framework called $λ$DD, which identifies the most expressive model, $λ$DD-O-NUCX, suitable for dense and sparse Boolean functions and invariant by negation, with formal canonicity verification in Coq and a linear bound on size gains.
We introduce a novel framework, termed $λ$DD, that revisits Binary Decision Diagrams from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like Chain-DD 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 $λ$DD-O-NUCX, is suitable for both dense and sparse Boolean functions, and is moreover invariant by negation. The canonicity of $λ$DD-O-NUCX is formally verified using the Coq proof assistant. We furthermore give bounds on the size of the different diagrams: the potential gain achieved by more expressive models can be at most linear in the number of variables n.