binary-decision-diagram - 多输出 BDD 的生成

Question

我正在使用 CUDD 包生成与输入基准文件相对应的 PLA 格式的 BDD。对于具有 3 个输入引脚（例如）和 5 个输出引脚（例如）的基准函数，我得到与 5 个输出相对应的 5 个输出 BDDS。但是，我想为整个基准测试功能生成一个多输出 BDD。有可能吗？....如果是这样，我如何使用 CUDD 包生成多输出 BDD。请帮忙。

Answer 1

这个有可能。让 B1、B2、B3、B4、B5 成为输入变量 x1、x2、x3 集合上的 BDD（在您的示例中）。您为输出和计算分配了一些额外的变量 y1, y2, y3, y4, y5

!(B1 ^ y1) & !(B2 ^ y2) & !(B3 ^ y3) & !(B4 ^ y4) & !(B5 ^ y5)

在变量 x1, ..., y5 上获得一个新的 BDD，它将所有变量估值映射为 true，其中 yi 是 {1,2,3,4,5} 中所有 i 在 x1 到 x3 上的 Bi 值。这应该是你想要的。

请注意，虽然 !(B ^ y) 看起来很奇怪，但编码的想法是我们应该让 y 的值是 B 的值。但是只有 XOR 运算符可用，我否定结果（在CUDD 中的恒定时间）来模拟相等性要求。