BDD minimization using symmetries

In this paper we study the effect of using information about (partial) symm etries for the minimization of reduced ordered binary decision diagrams (RO BDD'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 vi ew, Statistical results and benchmark results are reported to underline the efficiency of the approach. They prove that our techniques lead to improve ments of the ROBDD sizes by up to 70%.