问题标签 [binary-decision-diagram]

计算两个零抑制二元决策图连接的算法是什么？

我已经找了好几个小时了，就是找不到。据我所知，它也不在 Knuth 的书中，尽管它确实给出了结果的定义。

我宁愿不必涉足任何具体的实现；我发现实施细节非常分散注意力。

ZDD 的加入f和g是{ a ∪ b | a ∈ f and b ∈ g }

我有一组整数，表示为归约有序二进制决策图（ROBDD）（解释为一个函数，如果输入在集合中，则计算结果为真），我将调用 Domain 和一个整数函数（我将调用F) 表示为 ROBDD 的数组（结果的每一位一个条目）。

现在我想为 F 计算域的图像。这绝对是可能的，因为它可以通过枚举域中的所有项目、应用 F 并将结果插入图像中来轻松完成。但这是一个具有指数复杂性（与域大小呈线性关系）的可怕算法，我的直觉告诉我它可以更快。我一直在研究以下方向：

1. 将 Restrict(Domain) 应用于 F 的所有位
2. 做魔术

但事实证明，第二步很困难。第一步的结果包含我需要的信息（至少，我有 90% 的把握），但形式不正确。是否有一种有效的算法将其变成“编码为 ROBDD 的集合”？我需要其他方法吗？

我卡在CUDD（C接口）的BDD上的操作上，我不知道我们在计算图像时是否可以删除一些变量（从BDD的一个状态到另一个状态）以及如何传递结果BDD（最终BDD ) 要获取所有变量，有人可以告诉我我们是否可以通过 CUDD 做到这一点吗？干杯

谁能告诉我是否可以安全地从 CUDD 的经理中删除变量？例如：我通过v1 = Cudd_bddNewVar(manager);注册了两个变量 和v2 = Cudd_bddNewVar(manager)。我可以v2从管理员中删除吗？

有人对 Java 中的 BDD（二进制决策图）实现（或提供 Java 绑定的实现）有建议吗？我在网上找到了这个页面：http: //www.mancoosi.org/~abate/avalaible-bdd-libraries但不确定它是否已过时。还是只使用 Prolog 实现有意义？

我正在尝试使用 ZDD 实现单变量多项式，正如另一个问题的评论中所建议的那样。

我读过 S. Minato 的论文（你可以在这里下载），但我不明白如何在这些 ZDD 上实现操作。

论文中的想法是多项式可以用x^(2^i)变量来表示。例如x^5 + x^3 + x可以重写为x^4x^1 + x^2x^1 + x^1，如果您为每个x^(2^i)变量创建节点并与相乘的“1-edge”变量和相加的“0-edge”变量连接，您可以轻松获得表示该多项式的图形. ZDD 是在图上强制执行某些条件的此类图（有关更多信息，请阅读 Minato 的文章和关于 BDD的维基百科页面）

系数可以类似地使用 2 的幂和来表示（例如5 = 2^2 + 2^0等。每个2^i都是变量，并且节点以相同的方式与 1 和 0 边连接）。

现在，我的问题是添加两个 ZDD 的算法。算法看起来很简单：

如果 F 和 G (ZDD) 没有共同的组合，则加法 (F + G) 只需合并即可完成。当它们包含一些常见的组合时，我们计算以下公式： (F + G) = S + (Cx2)，其中 C = F ∩ G, S = (FUG) \ C 。通过重复这个过程，最终会用尽常见的组合并完成该过程。

问题是：如何有效地找到“C”和“S”？

作者提供了乘法的代码，但是一旦你实现了前面的算法，代码实际上是微不足道的。而且由于没有提供这些算法，因此乘法运算也是“无用的”。

此外，“合并”ZDD 的概念也没有得到很好的解释，尽管考虑到变量的顺序应该是一致的，只有一种方法可以将图合并在一起，而且维持这种顺序的规则可能很简单够了（我还没有将它们正式化，但我对它们有一个粗略的了解）。

假设我使用 BDD 来表示关系中的元组集。为简单起见，考虑具有 0 或 1 值的元组。例如：R = {<0,0,1>, <1,0,1>, <0,0,0>} 表示 BDD 中的三元关系，它具有三个变量，例如 x、y 和 z（一个用于每个元组的元素）。我想要的是实现一个操作，给定一个像 R 的 bdd 和一个多维数据集 C 在 C 中的变量被抽象时返回包含唯一元组的 R 的子集。

例如，如果 C 包含变量 x（表示每个元组中的第一个元素），则函数的结果必须是 {<0,0,0>}。请注意，当 x 被抽象出来时，元组 <0,0,1> 和 <1,0,1> 变得“相同”。

现在假设 R = {<0,0,1>, <1,0,1>, <0,0,0>, <1,0,0>} 我们想再次抽象 x。在这种情况下，我希望结果是常量 false，因为在抽象 x 之后 R 中没有唯一的元组。

非常感谢任何帮助。

是否有一个软件包（最好是应用程序，而不是库）可以从给定的真值表（以某种文本格式）创建归约有序二进制决策图（ROBDD）？

我试图比简单的英语句子更正式地表达规则，并希望在使用命题方法和某种二元决策树来说明规则方面有一些方向。

假设指定区域之外的对象需要处于特定状态（例如redState）才能被考虑safe。用通俗易懂的英文句子表达；

如果对象在 ZoneA 之外并且处于 RedState，那么它是安全的，

但是，在某些情况下，对象可能不受此限制：

如果对象在 ZoneA 之外，不处于 RedState 并且是 Exempt 的，那么它是安全的。

如果对象在 ZoneA 之外，不处于 RedState 并且不是 Exempt，那么它不是安全的。

区域 A 中的对象是否处于红色状态并不重要。剩下的规则是：

如果一个对象包含在区域 A 中，那么它是安全的。

使用命题公式，我认为这些规则可以表示为

¬ InZoneA∧ RedState⇒Safe

¬ InZoneA∧ ¬ RedState∧ Exempt ⇒Safe

¬ InZoneA∧ ¬ RedState∧ ¬ Exempt ⇒ ¬Safe

工业区A⇒Safe

我咨询过系统规范方法（例如 Z），但更感兴趣的是传达规则的简明概念，而不是确保它们在更大的系统中运行。因此，我想将它们表示为一种二元决策树（图）。我已经阅读了有关该主题的一些注释，但有点不确定它们的使用是否是最好的方法，或者我是否正在屠杀它们。我对这些规则得出的表示形式如图所示，实线表示True，虚线表示False。

我非常感谢您就这种表示是否正确或我的方法/想法是否有缺陷提供意见。非常感谢！

windows中是否有任何二进制决策图（BDD）可用。我试图在vc++6.0中运行cudd ..提到链接 http://web.cecs.pdx.edu/~alanmi/research/soft/softPorts .htm

但它不能正常工作。运行示例代码时出现编译器错误