使用 CUDD 的两个 BDD 的交集答案

【问题标题】：Intersection of two BDDs using CUDD使用 CUDD 的两个 BDD 的交集
【发布时间】：2016-08-19 03:03:54
【问题描述】：

我想为以下两个布尔函数找到两个 BDD 的交集：

F=A'B'C'D'=1
G=A XOR B XOR C XOR D=1

这是我的代码：

 int main (int argc, char *argv[])
    {
        char filename[30];
        DdManager *gbm; /* Global BDD manager. */
        gbm = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0); /* Initialize a new BDD manager. */
        DdNode *bdd, *var, *tmp_neg, *tmp,*f,*g;
        int i;
        bdd = Cudd_ReadOne(gbm); /*Returns the logic one constant of the manager*/
        Cudd_Ref(bdd); /*Increases the reference count of a node*/

        for (i = 3; i >= 0; i--) {
          var = Cudd_bddIthVar(gbm,i); /*Create a new BDD variable*/
          tmp_neg = Cudd_Not(var); /*Perform NOT Boolean operation*/
          tmp = Cudd_bddAnd(gbm, tmp_neg, bdd); /*Perform AND Boolean operation*/
          Cudd_Ref(tmp);
          Cudd_RecursiveDeref(gbm,bdd);
          f = tmp;
        }

        for (i = 3; i >= 0; i--) {
          var = Cudd_bddIthVar(gbm,i); /*Create a new BDD variable*/
          tmp = Cudd_bddXor(gbm, var, bdd); /*Perform AND Boolean operation*/
          Cudd_Ref(tmp);
          Cudd_RecursiveDeref(gbm,bdd);
          g = tmp;
        }
        bdd= Cudd_bddIntersect(gbm,f,g);/*Intersection between F and G */
        bdd = Cudd_BddToAdd(gbm, bdd); /*Convert BDD to ADD for display purpose*/
    print_dd (gbm, bdd, 2,4); /*Print the dd to standard output*/
    sprintf(filename, "./bdd/graph.dot"); /*Write .dot filename to a string*/
    write_dd(gbm, bdd, filename);  /*Write the resulting cascade dd to a file*/
    Cudd_Quit(gbm);
    return 0; 
}

这是我得到的结果：

DdManager nodes: 7 | DdManager vars: 4 | DdManager reorderings: 0 | DdManager memory: 8949888 
: 3 nodes 2 leaves 2 minterms
ID =  0xaa40f   index = 0   T = 0           E =  1        

0---  1

正如您在此处看到的那样，交叉点给出 A=0 并且不关心 B、C 和 D。我期望 A、B、C 和 D 的值同时满足 F 和 G。但显然 A=0不是 F 和 G 的解决方案。例如，有人可以选择 A=0,B=1，它为函数 F 提供 0。这里有什么问题？

【问题讨论】：

标签： binary-decision-diagram cudd

【解决方案1】：

这个回复来得太晚了，但为了结束这个问题，问题是Cudd_bddAnd 和Cudd_bddXor 的最后一个操作数是bdd 而不是f 或g。当然f和g都应该正确初始化（bdd当前初始化的方式）。以这种方式修复代码还将处理 bdd 的多次取消引用，如果垃圾收集启动，这将导致悲痛。

另外，Cudd_bddIntersect 不计算两个 BDD 的 AND，而是一个隐含 AND 的函数。当人们想要见证两个 BDD 的合取的非空性而不计算整个结果（然后可能从中提取见证）时使用它。

最后，bdd 既用作Cudd_BddToAdd 的操作数，又用作返回值的目的地。这保证会“泄漏”BDD 节点。

【讨论】：