1

我正在尝试使用Cudd_bddIte来实现简单的 BDD。以下代码按预期工作，给出图片中的图表（代表 node bdd）：

DdNode *v1 = Cudd_bddNewVar(gbm);
Cudd_Ref(v1);

DdNode *v2 = Cudd_bddNewVar(gbm);
Cudd_Ref(v2);

DdNode *v3 = Cudd_bddNewVar(gbm);
Cudd_Ref(v3);

DdNode *tmp1 = Cudd_bddIte(gbm, v1, Cudd_ReadLogicZero(gbm), Cudd_ReadOne(gbm));
Cudd_Ref(tmp1);

DdNode *tmp2 = Cudd_bddIte(gbm, v2, tmp1, Cudd_ReadOne(gbm));
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(gbm,tmp1);

DdNode *bdd = Cudd_bddIte(gbm, v3, tmp2, Cudd_ReadOne(gbm));
Cudd_Ref(bdd);
Cudd_RecursiveDeref(gbm,tmp2);

在此处输入图像描述

但是，如果我将 ITE 语句更改为tmp2以下

DdNode *tmp2 = Cudd_bddIte(gbm, v2, tmp1, Cudd_ReadLogicZero(gbm));

我得到了这个意想不到的图表：

在此处输入图像描述

对我来说，这是错误的，因为我希望最顶层的变量在为假时仍会立即产生 1，如第一张图片所示。我究竟做错了什么？

4

1 回答 1

2

在 (RO)BDD 中，所有变量都以特定顺序出现。在您的情况下，您按此顺序分配的顺序似乎是“v1、v2、v3”，并且似乎没有发生变量重新排序。

Cudd_bddIte 函数不要求您在构建 BDD 时遵守顺序。当您在代码中使用 bddIte 函数时，您将使用此功能：为了构建“bdd”，您使用 v1 和 v2 上的两个子树将 bddIte 函数应用于变量 v3。但是，v3 位于变量顺序的末尾，因此整个树都进行了重组。

事实上，您展示的第二棵树具有您所期望的属性：只要 v3 具有 TRUE 值，BDD 就会将变量评估映射到 TRUE。这可以从以下事实看出，到达“0”sink的唯一途径是通过节点0x2e，这是针对变量v3的，并且只有在取节点的then-successor时才能到达“0”sink。

于 2018-09-16T08:55:45.920 回答