In this paper we study the effect of using information about (partial) symmetries for the minimization of reduced ordered binary decision diagrams (ROBDD's). The influence of symmetries for the integration in dynamic variable ordering is studied for both completely and incompletely specified Boolean functions. The problems above are studied from a theoretical and practical point of view. Statistical results and benchmark results are reported to underline the efficiency of the approach. They prove that our techniques lead to improvements of the ROBDD sizes by up to 70%.

This paper investigates the sizes of symmetric variable order based reduced binary decision diagrams for partially symmetric Boolean functions. It gives exact bounds for the maximum number of nonterminal vertices for the cases that the set of symmetric variables is treated as block which is located either at the front or at the back of the variable order.

Addresses the problem of the detection of symmetries of Boolean functions. To know these symmetries may be important in several stages of logic design, e.g. in logic optimization, in logic synthesis, and in technology mapping. Reduced ordered binary decision diagrams (ROBDDs) play an important role in these tools. Using this representation form for Boolean functions there is a simple symmetry test by checking if certain cofactor functions are equivalent, i.e. if their ROBDD representations are the same. Unfortunately, this procedure may be very time and storage consuming because of the necessary cofactor computations. The approach presented in this paper uses preprocessing methods to find as many asymmetric pairs of variables as possible to avoid cofactor computations at the end. For that, special properties of the ROBDD structure as well as properties of Boolean functions are used. Experimental results on a large number of benchmarks show that this is a very efficient approach.