论文标题
BDD的大小的下限证明代表移位的添加
Lower Bound Proof for the Size of BDDs representing a Shifted Addition
论文作者
论文摘要
决策图（DDS）是布尔函数最流行的表示之一。它们被广泛用于电路的设计和验证。已证明，不同类型的DDS代表多项式空间中的重要功能，某些类型（例如二进制决策图（BDDS））也允许在多项式时间内对图进行操作。但是，没有被证明能够在多项式空间中代表多项式空间中的任意布尔函数的类型。特别是对于BDD，众所周知，整数乘法是输出BDD具有指数大小的功能之一。在本文中，我们表明，这也适用于整数添加，其中一个操作数被任意值向右移动。我们将此功能称为移动的添加。我们对此功能的兴趣是通过在浮点增加过程中发生的。
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.
