Abstract:
Ordered binary decision diagrams (OBDDs) are nowadays the most common dynamic data structure or representation type for Boolean functions. Among the many areas of application are verification, model checking, computer aided design, relational algebra, and symbolic graph algorithms. Although many even exponential lower bounds on the OBDD size of Boolean functions are known, there are only few functions where the OBDD size is even asymptotically known exactly. In this paper the exact OBDD sizes of the fundamental functions multiplexer and addition of n-bit numbers are determined.