我有一个包含值的 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 种表示形式。有什么方法可以让我只做一个吗？
你有各种可能性。在下文中，我主要重复负数的二进制补码表示的动机（https://en.wikipedia.org/wiki/Two%27s_complement）。
对所有数字使用相同的位数，例如用 8 位写入所有数字，然后使用第一位作为符号
6 = 00000110
-5 = 10000101
4 = 00000100
数字零将有两种表示形式：00000000 和 10000000（+0 和 -0）。如果您使用 ZDD（零抑制 BDD）而不是普通的 ROBDD，您将获得非常紧凑的表示。
使用符号的最后一位，这对于执行算术来说非常棘手，但对于表示来说不是问题。
6 = 1100 (110 + 0)
-5 = 1011 (101 + 1)
4 = 1000 (100 + 0)
您可以设置规则，即第一个（最左边的）位必须始终为 1。在这种情况下，数字 0 唯一地表示为 1。ROBDD 将使它成为一个紧凑的表示。