Lower Bound Proof for the Size of BDDs representing a Shifted Addition

TL;DR

This paper proves that BDDs require exponential size to represent the shifted addition function, extending known limitations of BDDs in representing certain arithmetic functions, especially relevant in floating point operations.

Contribution

The paper establishes a lower bound on the size of BDDs for shifted addition, a previously unproven function, highlighting fundamental limitations of BDDs in representing shifted arithmetic operations.

Findings

Shifted addition requires exponential BDD size.

Extends known exponential size results to shifted arithmetic functions.

Implications for BDD-based circuit verification and floating point arithmetic.

Abstract

Decision Diagrams(DDs) are one of the most popular representations for boolean functions. They are widely used in the design and verification of circuits. Different types of DDs have been proven to represent important functions in polynomial space and some types (like Binary Decision Diagrams(BDDs)) also allow operations on diagrams in polynomial time. However, there is no type which was proven capable of representing arbitrary boolean functions in polynomial space with regard to the input size. In particular for BDDs it is long known that integer multiplication is one of the functions, where the output BDDs have exponential size. In this paper, we show that this also holds for an integer addition where one of the operands is shifted to the right by an arbitrary value. We call this function the Shifted Addition. Our interest in this function is motivated through its occurrence during the floating point addition.