Implicit Manipulation of Polynomials Based on ZBDDs

Abstract

In this chapter, we present a good application of ZBDDs, that manipulates arithmetic polynomial formulas containing higher-degree variables and integer coefficients. In this method[Min95], we can represent large-scale polynomials compactly and uniquely, and can manipulate them in a practical time. Constructing canonical forms of polynomials immediately leads to equivalence checking of arithmetic expressions. Since polynomial calculus is a basic part of mathematics, our method is expected to be useful for various problems.