Exact minimization of determinant decision diagrams

Determinant decision diagram (DDD) is a canonical and compact representation of symbolic expressions in the form of circuit matrix determinants and cofactors for symbolic circuit analysis. DDD-based symbolic analysis algorithms have time and space complexities proportional to the number of DDD vertices. In this paper, we first present a theoretical characterization of the worst-case complexity of the minimal DDDs. We then present an exact algorithm to minimize the number of DDD vertices incorporating both a lower bound and upper bound for pruning the search space. Experimental results are presented to demonstrate the effectiveness of the proposed algorithm and the validity of theoretical analysis.