Mathematical model to predict the number of nodes in an ROBDD

This paper analyses and describes the relation between the size of a Boolean function and the number of nodes in its ROBDD representation. Knowing the number of variables and the number of product terms of a Boolean function, we can predict the number of nodes in its reordered binary decision diagram (ROBDD) without building the BDD. A mathematical model for this prediction has been developed. This model can be used to find the maximum number of nodes that can be produced for a given number of variables. The model can also be used to find the number of product terms above which the ROBDD is reduced to 1 node only. We demonstrate that the predictions using this model are quite promising, fast and easy to implement.