Worst-case and median encoding sizes of binary decision diagrams

Abstract

Binary decision diagrams (BDDs) have been a huge success story in hardware and software verification. In various extended forms, they are increasingly applied to a wide range of combinatorial problems. However, BDDs are a heuristic to encode Boolean functions of a fixed number of Boolean variables, so they cannot work well (i.e., require polynomial space) in all cases. We investigate the possible sizes, in particular the worst-case size and shape, of several BDD variants, including those with complement or swap flags. This work expands upon work previously done without complement or swap flags, and gives new combinatoric ways to count the exact distribution of BDD encoding sizes. Finally, this paper explores the expansion of such techniques into non-Boolean functions - specifically functions on the naturals