如何区分二进制决策图的正整数和负整数

Question

我有一个CSV文件，里面有值，我目前正在制定一个命题公式。

这是一个示例：

x=6,y=-5,z=4.
6 = 110
-5 = 1101 
4 = 100

我的公式：

( (x2 and x1 and not (x0)) and (y3 and y2 and not(y1) and y0) and (z2 and not(z1) and not(z0)) )

现在我用同样的方法生成一个BDD。如果我想让人/嵌入式系统从我的图中理解，1101可以表示为13或-5。任何负数都可以有2个表示形式。有没有办法让我只能去一个？

Answer 1

您有各种各样的可能性。在下文中，我主要重复负数的二补码表示的动机(https://en.wikipedia.org/wiki/Two%27s_complement)。

1. 对所有数字使用相同数量的位，例如，用8位写入所有数字，然后将第一位用于符号

   6 = 00000110
   -5 = 10000101 
   4 = 00000100
   

数字0将有两种表示形式：00000000和10000000(+0和-0(。如果你使用ZDD(零抑制BDD(而不是普通的ROBDD，你会得到非常紧凑的表示。

2. 使用符号的最后一位，这对于执行算术来说非常棘手，但对于表示来说不是问题。

   6 = 1100 (110 + 0)
   -5 = 1011 (101 + 1) 
   4 = 1000 (100 + 0)
   

您可以设置规则，即第一个(最左边的(位必须始终为1。在这种情况下，数字0被唯一地表示为1。ROBDD将使其成为一个紧凑的表示。

3. 使用二的补码，请注意，这需要固定位数，与第一个方案相同