CUDD Summe von Produkten Booleschen Ausdruck

Question

Ich mag würde BDD für die folgende Boolesche Funktion erstellen:

F = (A'B'C'D') OR (A'B C) OR (C' D') OR (A) 

ich nur F = (A'B'C'D') mit dem folgenden Code erstellen zu verwaltende aber wie andere Produktterme an die bestehenden BDD hinzufügen?

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; 
    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); 
     bdd = tmp; 
    } 

    bdd = Cudd_BddToAdd(gbm, bdd); 
    print_dd (gbm, bdd, 2,4); 
    sprintf(filename, "./bdd/graph.dot"); 
    write_dd(gbm, bdd, filename); 
    Cudd_Quit(gbm); 
    return 0; 
} 

Answer 1

Bauen jede Verbindung unabhängig, so dass Sie conj0 zu conj3 stellen Sie sicher, erhalten nur die richtigen Literale negieren. Ich bin nicht besonders versiert in C und habe gerade keine Entwicklungsumgebung eingerichtet, so dass Sie einige Korrekturen vornehmen müssen.

werde ich die folgende Abbildung

A <=> BDD(0) 
B <=> BDD(1) 
C <=> BDD(2) 
D <=> BDD(3) 

Build-conj0 so, wie Sie es jetzt in Ihrer for-Schleife zu tun verwenden. Stellen Sie danach conj0 = bdd sicher.

Für conj1 die (A' B C) Verwendung

bdd = Cudd_IthVar(gbm, 0); 
bdd = Cudd_Not(bdd); 
tmp = Cudd_And(gbm, bdd, Cudd_IthVar(gbm, 1)); 
Cudd_Ref(tmp); 
Cudd_Deref(gbm, bdd); 
bdd = tmp; 
tmp = Cudd_And(gbm, bdd, Cudd_IthVar(gbm, 2)); 
Cudd_Ref(tmp); 
Cudd_Deref(gbm, bdd); 
bdd = tmp; 
conj1 = bdd; 

Machen Sie dasselbe für conj2 und conj3 kodieren.

Nachdem Sie alle Konjunktionen erstellt haben, erstellen Sie die Top-Level-Disjunktion mit Cudd_bddOr(). Vergewissern Sie sich auch, dass Sie die Cudd_Ref() und Cudd_Deref() richtig erhalten, sonst wird Speicher verloren.

Answer 2

Wenn Sie daran interessiert sind nur in dieser bestimmten Funktion sind, hier ist ein Weg, es zu bauen und prüfen:

#include <stdio.h> 
#include <stdlib.h> 
#include "cudd.h" 

int main(void) { 
    /* Get set. */ 
    DdManager * mgr = Cudd_Init(4,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0); 
    DdNode *a = Cudd_bddIthVar(mgr, 0); 
    DdNode *c = Cudd_bddIthVar(mgr, 1); 
    DdNode *b = Cudd_bddIthVar(mgr, 2); 
    DdNode *d = Cudd_bddIthVar(mgr, 3); 
    char const * const inames[] = {"a", "c", "b", "d"}; 
    /* Build BDD. */ 
    DdNode * tmp = Cudd_bddIte(mgr, c, b, Cudd_Not(d)); 
    Cudd_Ref(tmp); 
    DdNode * f = Cudd_bddOr(mgr, a, tmp); 
    Cudd_Ref(f); 
    Cudd_RecursiveDeref(mgr, tmp); 
    /* Inspect it. */ 
    printf("f"); 
    Cudd_PrintSummary(mgr, f, 4, 0); 
    Cudd_bddPrintCover(mgr, f, f); 
    char * fform = Cudd_FactoredFormString(mgr, f, inames); 
    printf("%s\n", fform); 
    /* Break up camp and go home. */ 
    free(fform); 
    Cudd_RecursiveDeref(mgr, f); 
    int err = Cudd_CheckZeroRef(mgr); 
    Cudd_Quit(mgr); 
    return err; 
} 

Hinweis die Wahl der (optimal) mit variabler Reihenfolge. Sie sollten diese Ausgabe sehen:

f: 5 nodes 1 leaves 12 minterms 
1--- 1 
-11- 1 
-0-0 1 

a | (c & b | !c & !d)