关闭 CUDD 中 BDD 的补边

Posted 2023-03-31

【中文标题】关闭 CUDD 中 BDD 的补边

【英文标题】：Turn off complement edges for BDDs in CUDD

【发布时间】：2021-12-31 11:53:39

【问题描述】：

我查看了 CUDD (http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddIntro.html) 的在线文档，这是一个二进制决策图 (BDD) 库，但找不到关闭自动使用 BDD 补边的方法。在我看来它确实应该存在，你知道它是否存在吗？

【参考方案1】：

CUDD 中不存在此功能，因为补边的使用在每个 BDD 操作函数中都是作为非可选功能实现的。

目前还不清楚它有什么用处。 CUDD 的功能不会因关闭补边而改变。如果您的兴趣是不让互补边出现在 BDD 的可视化中，那么编写一个区分互补节点和非互补节点的可视化函数会更有意义，这是可能的（并且之前已经完成）并摆脱了补充的 else 边缘。

【讨论】：

嘿，感谢您的回答，我需要它来测试没有补边的 BDD 的大小。我将不得不在我的研究项目中找到解决方法..

@DanielMiedema 也许确实有一个简单的解决方法。构建自己的函数来计算 BDD 的节点数并不难，它分别考虑节点和互补节点，这样如果一个节点出现互补和非互补，它就会被视为两个节点。但是请注意，变量重新排序启发式算法在补充 else 边的情况下可能会有所不同，因为它们会在不同的时间触发重新排序（并且可能会略有不同的优化）。