c - Cudd_bddIte的意外输出

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

我得到了这个意外的图表：

对我来说，这是错误的，因为我希望最上面的变量仍然立即产生1，如果是错误的，如第一张图片所示。我做错什么了？

最佳答案

在（RO）BDD中，所有变量都以一定的顺序出现。在您的例子中，顺序似乎是“v1，v2，v3”，正如您在这个顺序中分配的那样，并且似乎没有发生变量重新排序。
Cudd_bddIte函数不要求在构建BDD时遵守顺序。在代码中使用bddIte函数时，可以使用此功能：对于构建“bdd”，可以使用v1和v2上的两个子树将bddIte函数应用于变量v3。但是，v3位于变量顺序的末尾，因此整个树被重新构造。
实际上，您显示的第二棵树具有您所期望的属性：每当v3有一个TRUE值时，BDD就会将变量值映射为TRUE。这可以从这样一个事实看出，到达“0”接收器的唯一方法是通过节点0x2e（对于变量v3），并且只有在获取节点的后续节点时才能到达“0”接收器。

关于c - Cudd_bddIte的意外输出，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/52337722/