Minimizing the number of paths in BDDs

BDDs are used in several fields as e.g. formal verification or synthesis. Minimizing the number of nodes in a BDD is a common technique, to reduce the memory needed to express a function. But recently applications like SAT-solving or synthesis have been shown to benefit from a small number of paths in a BDD. Here we present an algorithm and its implementation to carry out the minimization of a BDD with respect to the number of paths. After showing the existence of functions that can not be represented by a BDD that is minimal in the number of nodes and the number of paths at once, statistical experiments on the ISCAS89 benchmark set show the efficiency of the technique. In another set of experiments, the minimization of numbers of paths is compared to that of the number of nodes.