问题标签 [cudd]

我正在尝试使用 CUDD 查找 Shared-BDD 中的节点总数。 我已经使用 BuDDy-2.4 编写了 C 代码并且运行良好但是当我使用 CUDD 而不是 BuDDy 时，我的程序显示错误。

我的 BuDDY C 文件是：

我的 CUDD C 程序是：

但是这个 CUDD C 程序显示错误

我最近才开始使用 CUDD。

我有一个 BLIF 格式的电路，我想将它输入到 CUDD，我知道它会给我 BDD，我也想要 ZDD。

我已经阅读了自述文件，但是对于我的生活，我根本找不到如何使用它。

谁能告诉我如何详细输入 blif 到 CUDD？（什么命令以及在哪里编写命令）

对不起，如果这太基本了。

Does anyone on this community have experience with compiling linking the CUDD package for manipulating BDDs? Seems like a great resource if I can only compile something simple... Getting a lot of following. I am a novice with C, mainly Py guy, so any help would be highly appreciated. (I've tried using tulip-dd in Py, but that is a limited experience). Thanks in advance.

是否有使用 CUDD（不要与 CUDA 混淆）来操作 BDD 的经验的人知道为什么我可能不断收到可怕的“分段错误（转储核心）”。我怀疑这可能与引用取消引用有关，我承认我不完全理解。任何提示指针表示赞赏。我（评论了我一直在尝试的一些事情）：

我正在与（https://github.com/ivmai/cudd）合作，目标是执行以下重复过程：

(1) 输入：（相干，非递减）布尔函数表达式 top = a_1 a_2 a_3...+ x_1 x_2 x_3... + z_1 z_2 z_3...）。我正在使用的布尔值有数千个变量（ai...zj）和数百个术语。

(2) 处理：将布尔值转换为 BDD 以简化最小项或互斥割集（我们在可靠性世界中称之为）的计算。

(3) 输出：取一组我的最小割集（minterms）。通过将 (2) 中找到的所有小项相加来计算顶部事件概率。

我找到了一种使用劳动密集型手动 C 接口来构建布尔值的方法。我还发现了如何使用出色的 tulip-dd Py 界面来实现它，但无法像 cudd 那样进行扩展。

现在我希望通过 cudd 的 C++ 接口，我可以两全其美（我要求太多了吗？）也就是说，tulip-dd 的便利性和 cudd 的可扩展性。所以这里有一些示例代码。我失败的地方是第 3 步，打印出我以前可以在 C 中完成的最小术语。我如何使用 C++ 接口来完成它？！请参阅代码中的注释以了解我的具体想法和尝试。

谢谢，桂

我之前的帖子CUDD C++ Interface for convert Booleans to BDDs and result set of minterms (to cutsets)的后续文章。

在 Python 上运行的 tulip-dd BDD 库中，可以将布尔表达式定义和读取为字符串。这使得整个 I/O 过程非常方便。

现在，我们刚刚在上一篇文章中看到，使用 cudd C++ 接口，我们可以使用紧凑的数学符号方便地定义一个布尔表达式，例如x1*x2 + x3*x4以及如何从该表达式产生最小项的总和。但是 cudd 是否也允许我们将字符串用于布尔表达式？我怀疑不是，如果不是，我将不得不找到一种方法将上面 sum 乘积的字符串等价转换为等价的 Boolean: "x1*x2+x3*x4"to x1*x2+x3*x4。

我正在使用 CUDD ( https://github.com/ivmai/cudd ) 使用 bdd 和 zdd 功能进行模型检查，我想知道如何量化 zdds。

对于 bdd，有 bddExistAbstract 和 bddUnivAbstract 函数（参见http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddAllDet.html#Cudd_bddUnivAbstract）。

该手册说，这些函数普遍地和存在地从 bdd 中抽象出给定的变量（以封面形式）。我不太清楚“抽象出来”是什么意思，因此我坚持弄清楚量化如何改变 zdds。

你们能帮忙吗？谢谢。

这可能是本论坛常驻 CUDD/BDD 专家@DCTLib 的问题，但如果其他人有见解，当然欢迎！

考虑给定的最小项，例如： 0--0---0--0---0----11 1 。

我需要单独取每个 minterm 并用 P(x_i) 替换“1”（我正在处理变量的概率），用 1-P(x_i) 替换 0，用 1 替换“-”。然后我将其中的因素相乘一个最小项，P(x_i)...(1-P(x_j)) 并将它们加起来以获得顶部事件的概率。（对应于最小项的概率的和积）

我需要一一处理的原因是我正在处理会炸毁内存的大文件。一旦我超过 80-100 个变量，您就处于整个 minterm 文本文件转储大小的 TB OoM 中. 如果可能，我想获取每个 minterm，将其添加到运行总和中，并在添加后将其删除。

希望这很清楚，但如果不是，可能需要一些迭代。谢谢，

这是@DCTLib 在下面的帖子中提出的建议的后续行动。

Cudd_PrintMinterm，访问产品总和中的各个最小术语

我一直在追求建议的 (b) 部分，并将在单独的帖子中分享一些伪代码。

同时，在他的 (b) 部分建议中，@DCTLib 发布了指向https://github.com/VerifiableRobotics/slugs/blob/master/src/BFAbstractionLibrary/BFCudd.cpp的链接。我一直在尝试阅读这个程序。Somenzi 的经典论文 Binary Decision Diagrams 中有一个递归函数，它描述了一种计算满足分配数量的算法（下图，图 7）。我一直在尝试比较两者，蛞蝓和图 7。但很难看到任何相似之处。但是C对我来说几乎是不可思议的。你知道蛞蝓 BFCudd 是否基于 Somenze 图 7，@DCTLib？

谢谢，桂

对于那里的 CUDD 大师，我实际上使用的是 Python 等价物 tulip-dd： https ://github.com/tulip-control/dd 。

我正在尝试绘制由以下定义的 MDD 或多状态决策图：

我的问题之一是如何绘制 MDD。我试过了：

但是自动机没有这样的方法。