CUDD сумма произведений логическое выражение

Question

Я хотел бы создать BDD для следующей логической функции:

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

Мне удалось создать только F = (A'B'C'D') с помощью следующего кода, но как добавить другие термины продукта в существующий BDD?

 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

Создайте каждое соединение независимо, так что вы получите conj0 в conj3 убедитесь, что только отрицательные правильные литералы. Я не особенно разбираюсь в C и не имею настройки среды разработки прямо сейчас, поэтому вам нужно будет внести некоторые исправления.

Я буду использовать следующее отображение

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

строить conj0 То, как вы делаете это сейчас в вашем цикле. Удостовериться conj0 = bdd после этого.

За conj1 который будет кодировать (A' B C) использование

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;

Сделать то же самое для conj2 а также conj3,

После того, как вы получите все соединения, создайте дизъюнкцию верхнего уровня, используя Cudd_bddOr(), Также убедитесь, что вы получите Cudd_Ref() а также Cudd_Deref() правильно, иначе вы потеряете память.

Answer 2

Если вас интересует только эта конкретная функция, вот способ ее создания и проверки:

#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;
}

Обратите внимание на выбор (оптимального) переменного порядка. Вы должны увидеть этот вывод:

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

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