Exponential Lower Bounds on the Size of Variants of OBDD Representing Integer Division

摘要

An Ordered Binary Decision Diagram (OBDD) is a directed acyclic graph representing a Boolean function. The size of OBDDs largely depends on the variable ordering. In this paper we show the size of the OBDD representing the I-th bit of the output of n-bit-bit integer division is Ω(2~(n-i)/8) for any variable ordering. We also show that ∨-OBDDs, ∧-OBDDs and +-OBDDs representing integer diviasion has the same lower bounds on the size. We develop new methods for proving lower bounds on the size of ∨-OBDDs, ∧-OBDs and +-OBDDs.