Implicit manipulation of polynomials using zero-suppressed BDDs

We present a new technique that broadens the scope of BDD application. It involves manipulating arithmetic polynomials containing higher-degree variables and integer coefficients. Our method can represent large-scale polynomials compactly and uniquely, and it greatly accelerates computation of polynomials. As the polynomial calculus is a basic model in mathematics, our method is very useful in various areas, including formal verification techniques for VLSI design