How to group variables for reducing BDD

The reduced order binary decision diagram (ROBDD) is widely used in logic synthesis and verification due to its special characteristics. Most algorithms using ROBDD have polynomial runtimes in the size of the ROBDD. ROBDD varies with different variable orders. So, finding a variable order to make ROBDD small is meaningful in digital circuit design. In this paper, we introduce a novel method to utilize variable relations efficiently. Moreover, for the first time, relations among variable sets are used to reduce BDD further, which is neglected in the past. Experiment results show that our algorithm is effective to reduce ROBDD.