OKFDDs — Algorithms, Applications and Extensions

We present Ordered Kronecker Functional Decision Diagrams (OKFDDs), a graph-based data structure for the representation and manipulation of Boolean functions. OKFDDs are a generalization of Ordered Binary Decision Diagrams and Ordered Functional Decision Diagrams and as such provide a more compact representation of the functions than either of the two decision diagrams. We review basic properties of OKFDDs and study methods for their efficient representation and manipulation. These algorithms are integrated in our OKFDD package PUMA whose implementation is briefly discussed. Finally we point out some applications of OKFDDs, demonstrate the efficiency of our approach by some experiments and discuss a promising extension of the concept to also allow representation and manipulation of word-level functions.