Cudd_bddIte的意外输出

Question

我正在尝试使用Cudd_bddIte来实现简单的BDDs。下面的代码按照预期工作，给出了图片中的图表(表示节点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);

​

​

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

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

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

​

​

对我来说，这是错误的，因为我希望最上面的变量仍然会在false的情况下立即产生1，就像第一张图片中一样。我做错了什么？

Answer 1

在(RO)BDD中，所有变量都以特定的顺序出现。在您的例子中，顺序似乎是您分配的"v1，v2，v3“，并且似乎没有发生任何变量重新排序。

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

实际上，您所显示的第二个树具有您所期望的属性:每当v3具有真值时，BDD就会将变量valuation映射为TRUE。从以下事实可以看出这一点:到达"0“接收器的唯一途径是经由节点0x2e，其用于变量v3，并且只有当获取该节点的当时的后继者时才能到达"0”接收器。