路口使用CUDD

Question

2組的BDD的，我想找到兩個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.我expectin g，A，B，C和D的值同時滿足F和G.但顯然A = 0對於F和G都不是解。例如，某人可以選擇A = 0，B = 1，對於函數F給出0這裏有什麼問題？

Answer 1

這個回答來自實在太遲了，只是收的問題，問題是最後一個操作數既Cudd_bddAnd和Cudd_bddXor是bdd而不是f或g。當然，f和g都應該正確初始化（bdd目前的初始化方式）。通過這種方式修復代碼也將處理bdd的多個解除引用，這將導致應該垃圾回收的痛苦。

此外，Cudd_bddIntersect不計算兩個BDD的AND，但是暗含和。當人們想要證明兩個BDD的聯合沒有空缺而沒有計算出整個結果（然後可能從中提取一個證人）時，就會使用它。

最後，bdd被用作Cudd_BddToAdd的操作數和作爲返回值的目的地。這是保證「泄漏」BDD節點。