问题标签 [binary-decision-diagram]

假设以下定义：

我想从一个布尔表达式构建一个 ROBDD。到目前为止，我已经能够构建一个不满足无冗余或共享属性的 BDD。

命名和风格可能不是最好的，因为这仍在进行中。

节点在内部由唯一的 id 表示。它从 2 开始。左子树的根节点将标记为2n，右子树的根节点将标记为2n + 1。

该函数将布尔表达式和表达式中出现的变量的索引列表作为输入。

例如，对于以下表达式：

电话buildBDD bexp [2,3,7]将返回

我已经进行了以下更改以说明无冗余属性（这尚未经过彻底测试，但似乎可以正常工作）

（请原谅上面的笨拙表达）

但是，我不知道如何处理共享属性，尤其是因为共享节点可能位于图中的任何位置，并且我没有存储当前树。如果需要，可以更改唯一节点 ID 的公式。

注意：这是一个练习，因此所涉及的类型和风格可能不是最佳的。我也不应该更改它们（尽管我可以自由更改功能）。

我们认为位矩阵是一个包含大小为 的整数行的(n x m)规则数组。nm

我查看了Hacker's Delight和其他来源，我为此找到的算法相当专业：具有 8x8、32x32、64x64 等两种大小的幂的方阵（这是正常的，因为机器是这样构建的）。

我想到了一种更通用的算法（对于任意nand m），在最坏的情况下，它具有预期的复杂性（我认为），但是对于包含大部分相似列或零多于一的矩阵，该算法似乎更有趣（在极端情况下，如果矩阵一遍又一遍地包含同一行，则它是线性的）。它遵循一种二元决策图操作。

输出不是转置矩阵，而是压缩转置矩阵：一个对列表，(V,L)其中L是int_m表示转置矩阵的行（通过设置相应位置的位）应包含int_n V. 未出现在任何对中的转置矩阵的行用 填充0。

例如，对于矩阵

有转置的

算法输出：

并且将这对读(100,0000101)作“将值100放在转置矩阵的第 5 行和第 7 行”的意思。

这是算法（用伪 OCaml/C 编写）和上例中算法的进度图。

我们将根据三元组来运行(index_of_current_line, V, L)，它的类型是(int, int_n, int_m)，其中int_n是 n 位宽整数的类型，并且int只是一个机器整数，其宽度足以容纳n。该函数获取这些三元组的列表、矩阵、行数和用于输出的累加器，(list of pairs (int_m, int_n))并在某个点返回该累加器。

转置函数的第一次调用是

取“&”、“|” "xor" 是通常的按位运算

请注意，如果矩阵的宽度大于高度，则它会更快（例如，如果 n = 3 和 m = 64）

我的问题是：

• 这有趣和/或有用吗？
• 我在重新发明轮子吗？
• “几乎为零”矩阵或“小微分线”矩阵是否足够常见以至于有趣？

PS：如果有什么不清楚的地方，请告诉我，我会重写任何需要的！

假设DdManager有四个变量：x, y, x', y'并且我有一个由xand构建的 BDD y。现在我想更改x为x', y,y'即获得由x'and构建的相同 BDD y'。

我怎样才能使用 CUDD 包得到这个？当我想实现模型检查算法时遇到了这个问题。我想知道如何实现这个操作或者我是否误解了符号模型检查算法？非常感谢！

我想知道将二进制公式转换为香农范式的步骤。

如何将其转换为香农范式？

我试图了解两个 ROBDD 的组合是如何工作的。

我需要找到一个公式，该公式F3是通过替换公式中所有出现的d公式F1来获得的F2。

我该如何继续解决这个问题？

我正在开发一种用于二元决策图的教学工具，其中还有一个变量重新排序的功能。任何人都可以建议一个合适的库来实现变量重新排序，同时构建树或某种实现相同的算法吗？

如果我可以使用像 pyeda、buDDy 或 pycudd 这样的库，那将是最好的，因为我已经熟悉这些库。

如果您需要任何澄清，谢谢并发表评论。

我知道 CUDD 支持 ADD（代数决策图），但我似乎无法弄清楚如何将 ADD 用于多个输出布尔函数。此类函数的 ADD 需要有多个叶子，每个叶子代表一个布尔输出向量（可能编码为整数）。例如，0101 为 5，1000 为 8 等等。有谁知道这样的 DD 是否可以在 CUDD 中构建？

这是我制作有序二元决策图的python代码（与上下文不太相关）。所以我只有一棵特定高度的树，我需要将一些叶子节点设置为一个。所以我有一个变量path，它涉及一个“决定”数组，从那个特定的节点向左或向右。但是我的代码错误地修改了多个根。我对 Python 还很陌生，我在使用 C 时曾经依赖指针。

我正在研究二元决策图的可变排序。到目前为止，我们已经使用了不可逆电路。但不是我们需要使用 Reversible Benchmarks 来实现一些方法。但是我没有任何方法可以使用 C 语言中的 CUDD 库来读取基准文件（例如 blif、kiss、slif 文件）。我已经在互联网上寻找可用资源。有人请帮我找出路。

我正在通过许可指南将产品系列表示为袋模型，其中还考虑了出现的情况以提出 BDD。

我正在尝试将类似的步骤包含在我的问题中。文字说

如果我们采用 bag-model，则实现类似于 set-model 实现，除了处理特征的重复。ROBDD 不允许节点重复。为了处理 BDD 本身中某个特征的出现次数，我们设计了对其进行编码的出现级别。我们对这个数字进行二进制编码。例如，如果我们有一个具有 3 个特征的产品：x、y 和 z，并且一个特征的最大出现次数是 7，那么我们需要三个二进制位对其进行编码。让产品系列 W 有一种产品，它具有三个 x 特征和六个 z 特征以及零个 y 特征。我们的产品系列包含一个产品 Pt，由图 3.7 中的 BDD 表示。代表这个包的 BDD 以类似于集合模型中的方式描述产品。然而，我们对包含 bl、b2 和 b3 的节点级别中的出现进行编码。我们在图 3.7 中读到，如果 x 存在于这个产品中，那么我们必须选择 bl 和 b2，而不是 b3。这是二进制代码 011，分别代表 b3、b2 和 bl，其中 x 出现三个。类似地，对于这个产品中存在的 y，我们得到二进制出现编码为 000，即 0 出现。对于 z，我们得到 110 的二进制出现，它带有数字 6。我们得到二进制出现编码为 000，即 0 次出现。对于 z，我们得到 110 的二进制出现，它带有数字 6。我们得到二进制出现编码为 000，即 0 次出现。对于 z，我们得到 110 的二进制出现，它带有数字 6。

因此，对于产品系列 Z = {{(x,3),(y,0),(z,6)}}，相应的 bdd 将是 ->

对于产品系列 W = {{(x,3),(y,1),(z,7)}}，BDD 将是

但是他是怎么想出这些BDD的，BDD肯定有一些基本的公式。您能否帮助我了解如何为给定的家庭得出相同的公式，以便我可以在其他用例中类似地进一步使用它。谢谢。