0

次の 2 つのブール関数の 2 つの 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 を気にしません。私は、F と G の両方を満たす A、B、C、および D の値を期待していました。しかし、明らかに A=0 はF と G の両方の解。たとえば、関数 F に 0 を与える A=0,B=1 を選択できます。ここで何が問題なのですか?

4

1 に答える 1

1

この返信は非常に遅くなりますが、問題を解決するために、問題は両方のCudd_bddAndandの最後のオペランドがorの代わりになってCudd_bddXorいることです。もちろん、両方とも適切に初期化する必要があります (ウェイは現在初期化されています)。この方法でコードを修正すると、 の複数の逆参照も処理されます。これは、ガベージ コレクションが開始された場合に問題を引き起こす可能性があります。bddfgfgbddbdd

また、Cudd_bddIntersect2 つの BDD の AND を計算するのではなく、AND を暗示する関数です。これは、結果全体を計算せずに 2 つの BDD の結合が空ではないことの証人が必要な場合に使用されます (そして、結果から証人を抽出する可能性があります)。

最後に、戻り値のbddオペランドCudd_BddToAddと宛先の両方として使用されます。これにより、BDD ノードが「リーク」することが保証されます。

于 2016-10-28T17:41:23.017 に答える