An anytime symmetry detection algorithm for ROBDDs

Detecting symmetries is crucial to logic synthesis, technology mapping, detecting function equivalence under unknown input correspondence, and ROBDD minimization. State-of-the-art is represented by Mishchenko´s algorithm. In this paper, we present an efficient anytime algorithm for detecting symmetries in Boolean functions represented as ROBDDs, that output pairs of symmetric variables until a prescribed time bound is exceeded. The algorithm is complete in that given sufficient time it is guaranteed to find all symmetric pairs. The complexity of this algorithm is in O(n⁴ + n|G| + |G|³ ) where n is the number of variables and |G| the number of nodes in the ROBDD, and it is thus competitive with Mishchenko´s O(|G|³ ) algorithm in the worst-case since n Lt |G|. However, our algorithm performs significantly better because the anytime approach only requires lightweight data structure support and it offers unique opportunities for optimization