问题标签 [binary-decision-diagram]

1 个决策树最多有 2^d 个节点，

n个决策树有多少个节点？

n*(2^d), 或 2^(nd), 或 1+2+...+2^d, 还是别的什么？

谢谢！

我正在使用 CUDD C++ 接口。

我没有找到关于这个图书馆的太多信息。

如何获得 BDD 的两个孩子？

例如：

现在，有了 f，我想得到它的 then 孩子和 else 孩子。文档说 DdNode 有这个孩子，但我不知道如何访问它们。

谢谢你。

我正在做一个程序校正/综合项目。我的任务是获取错误轨迹（反例），将其定位在完整的状态空间中，并在该位置修复模型。我想将其实现为 NuSMV 扩展。

我一直在调试 NuSMV 以了解和探索它的源代码。到目前为止，我已经找到了创建 BDD FSM 的方法（compile.c 第 520 行）。我试图找到一种遍历 bdd 的方法，以便以编程方式访问状态空间，从而对模型执行我的纠正工作。我还不能理解 NuSMV 用来通过 bdd fsm 验证属性的递归探索函数。

我想知道如何遍历 bdd 结构，以便通过 dot 等工具对其进行可视化。我还想知道是否已经制作了这样或类似的可视化（我已经搜索过但没有找到）。其次，我想验证我所采取的方向是否正确，或者是否有更好的方法来获得给定模型的完整状态空间，并探索它，特别是关于获得的反例通过 NuSMV。

我正在重新实现一个 ROBDD 库（为了好玩，一些工作和一个严重的 NIH 案例）。我想要一些其他库构建的“参考”图表来比较结果 [*]

例如，给定变量阶 x1 < y1 < x2 < y2，得到的图形是什么

(x1 <=> y1) /\ not (x2 <=> y2) /\ (x2 <=> y2) [**]

我假设标准运营商。另外，如果有帮助，我假设 /\ 是左关联的。

欢迎任何其他小例子。

谢谢

马可

[*] 我知道！我应该下载库，安装它们并使用它们，但我很懒。

[**] 该示例取自 Moeller 和 Oestergard 的示例，该示例在网上漂浮。

我有点困惑。我需要举例说明在每个布尔运算中使用 ITE 算法。但我其实不知道有多少？例如，我的意思是 AND、OR、XOR、XNOR、NOR、NAND、NOT。我不知道其他的......我至少错过了一个，因为它不可能是七次手术。(2^n)

我读了一篇名为基于功能决策图的多级逻辑综合的论文，它是关于功能决策图（FDD）的，它是二元决策图（BDD）的一种变体。在这一段中，有一段提到了“路径”：

作为一个重要的结果，可以观察到，即使节点数量几乎相同，与 BDD 相比，我们也减少了路径数量（参见表 1）。由于路径的数量等于规范的两级 RME 的 pi 项的数量，这意味着函数表示的复杂性降低。

我猜“路径”是指 BDD 或 FDD 中从根到终端的道路数量。

例如：

这个例子的路径是9（你可以检查一下）。

我的问题是这个参数或特征“路径”的意义是什么？

我正在尝试使用 PyEDA，我需要可视化二元决策图，我正在阅读此文档，但我无法理解！

这里它说：如果你的机器上安装了 GraphViz，并且 dot 可执行文件在你的 shell 路径上可用，你可以使用 gvmagic IPython 扩展来可视化 BDD。

首先，如何使 dot 可执行文件在我的 shell 路径上可用？

然后，在文档中我们有这部分：

这是DOT环境吗？

对不起，如果问题如此简单和愚蠢！我在使用 Linux 方面不是很专业。

这个问题是关于如何为符号模型检查器生成符号状态空间。首先，我介绍了一些让我想为 MDD 做这件事的背景，然后我更详细地解释了这个问题。

Edmund M. Clarke（模型检查的创始人之一）的本次讲座介绍了符号模型检查。它说“工业强度”模型检查器使用布尔编码（二进制决策图，或 BDD）来处理状态爆炸问题。但是，它只允许比常规模型检查多一个数量级的状态。我跳过了常规的模型检查，它直接构建程序 b/c 的状态转换图，我可以想象这立即是不切实际的。

我看过一些描述优于 BDD 质量的论文，例如处理更多状态1（避免？！状态空间爆炸问题），一般加速2（有界模型检查），使用状态匹配技术来限制状态空间搜索（超出有界模型检查）3，并使用 MDD，其执行速度比现有 BDD[4][5] 快几个数量级。

BDD将平均支持的状态数从大约 10^6 提高到 10^20。那篇论文还说：

不幸的是，众所周知，符号技术不适用于异步系统，例如通信协议，这些系统尤其受到状态空间爆炸的影响。

因此，MDD 甚至 EDD 似乎是模型检查的更好选择。还有边值 BDD (EVBDD)。但是我的问题是，如何为 ~MDD（或任何一个最好的）构建符号状态空间。本文档介绍了它，但似乎没有解释如何实际生成它。他们说：

我们使用准约简、有序、非负边值、多值决策图。

想知道是否可以从高层次上解释 MDD 的状态空间生成算法，以及系统中涉及的数据结构是什么，例如node对象的属性是什么（如 C 结构）。我在想，如果我能看到数据结构的总体情况以及算法的大致工作原理，那将足以实现。

另外，我不确定初始程序和规范需要做什么。因此，如果解释可以快速描述/介绍如何生成任何中间对象，那将是有帮助的。添加这个是因为我在一篇论文中看到他们有 Petri 网形式的程序，然后他们将其转换为 MDD，我不确定如何将程序转换为 Petri 网，或者是否有必要。基本上，如何从源代码到高级别的 MDD。

我认为这张图片是状态空间生成的算法，但我一直难以理解它的细节。具体来说，涉及的数据结构，以及“状态”的来源，即这些是来自其他模型的布尔谓词还是什么。

这个似乎也很接近：

以下是同一篇论文的更多内容：

(1)在本文中，我们展示了布尔决策过程，如 Stalmarck 方法 [16] 或 Davis & Putnam 过程 [7]，如何替代 BDD。这种新技术避免了 BDD 的空间爆炸，更快地生成反例，有时还加快了验证速度。

(2)本文的主要结果是在检查有时间限制的直到公式的时间复杂度上提高了 O(N)，其中 N 是所考虑的 CTMC 中的状态数。

(3)我们在之前的工作的基础上提出了符号执行和模型检查的组合，用于分析具有复杂输入的程序 [14,19]。在这项工作中，我们限制了输入大小和（或）模型检查器的搜索深度。在这里，我们超越了有界模型检查，我们研究了状态匹配技术来限制状态空间搜索。我们提出了一种检查符号状态何时被另一个符号状态包含的技术。

(4)我们提出了一种使用多值决策图生成异步系统状态空间的新算法。与相关工作相比，我们将系统的下一个{状态函数编码为单个布尔函数，而是作为整数函数的叉积。这允许应用各种迭代策略来构建系统的状态空间。特别是，我们引入了一种新的优雅策略，称为饱和度，并在工具 SMART 中实现它。除了通常比现有的基于 BDD 的状态空间生成器快几个数量级之外，我们的算法所需的峰值内存通常接近存储整个状态空间所需的最终内存。

(5)基于二进制决策图 (BDD) 的符号技术被广泛用于推理硬件电路和同步控制器的时间特性。然而，它们在处理基于交错语义的巨大状态空间底层系统时，通常表现不佳，例如通信协议和分布式软件，它们由通过共享事件进行通信的独立行动子系统组成......本文展示了通过利用许多基于事件和基于组件的系统模型的交错语义，可以极大地改进使用决策图的状态空间探索技术。

越来越接近这个：

可达状态空间 X_reach 可以表征为不动点方程 X ⊆ X_init ∪ T(X) 的最小解。算法Bfs正是实现了这种固定点计算，其中集合和关系分别使用 L 级和 2L 级 MDD 存储，即节点 p 编码具有特征函数 v_p 的集合 X_p 满足

v_p(i_L,...,i_1) = 1 ⇔ (i_L,...,i_1) ∈ X_p。

集合的并集通过对它们的特征函数应用 Or 运算符来简单地实现，而一步可达状态的计算通过使用函数 RelProd 来实现（当然，如果使用 MDD，则必须使用这些函数的 MDD 版本而不是 BDD）。由于它执行广度优先的符号搜索，算法 Bfs 停止的迭代次数与任何可达状态与初始状态的最大距离一样多。

假设我有以下布尔函数：

现在我想用它们构建一个二元决策图。我浏览了几篇论文，但还没有找到如何从像这样的嵌套逻辑公式中构造它们。

据说布尔函数是有根有向无环图。它有几个非终端和终端节点。然后它说每个非终端节点都由一个布尔变量（不是函数）标记，该变量有两个子节点。我不知道上面的函数定义中的布尔变量是什么。从节点到子节点的边a或分别b代表节点分配为 0 或 1。如果同构子图已合并，则称为归约，并且删除了两个子同构的节点。这是一个降序二元决策图（ROBDD）。

由此，以及我遇到的所有资源，我无法弄清楚如何将这些函数转换为 BDD/ROBDD：

或者也许是这些需要转换：

寻求帮助来解释我需要做什么才能将其变成有根、有向、无环图。了解数据结构的样子也会有所帮助。似乎只是这样：

但接下来的问题是如何从这些函数foo、bar和构建图形baz。

是否可以使用 CUDD 获得 (x0 ∧ x1 ) ∨ (x0 ∧!x1 ) ∨ (!x0 ∧ x1 ) ∨ (!x 0 ∧!x 1 ) 的 bdd，它仍然具有代表变量 x0 和 x1 的节点? 我知道上面的布尔公式简化为常数函数 1。但我仍然想要一个不简化公式但将其表示为对应于 x0 和 x1 的 BDD“包含”节点的 BDD。如果不在 CUDD 中，是否可以使用其他工具来执行此操作？