Неожиданный вывод Cudd_bddIte

Question

Я пытаюсь использовать Cudd_bddIte реализовать простые BDD. Следующий код работает, как и ожидалось, давая диаграмму на рисунке (который представляет узел bdd):

DdNode *v1 = Cudd_bddNewVar(gbm);
Cudd_Ref(v1);

DdNode *v2 = Cudd_bddNewVar(gbm);
Cudd_Ref(v2);

DdNode *v3 = Cudd_bddNewVar(gbm);
Cudd_Ref(v3);

DdNode *tmp1 = Cudd_bddIte(gbm, v1, Cudd_ReadLogicZero(gbm), Cudd_ReadOne(gbm));
Cudd_Ref(tmp1);

DdNode *tmp2 = Cudd_bddIte(gbm, v2, tmp1, Cudd_ReadOne(gbm));
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(gbm,tmp1);

DdNode *bdd = Cudd_bddIte(gbm, v3, tmp2, Cudd_ReadOne(gbm));
Cudd_Ref(bdd);
Cudd_RecursiveDeref(gbm,tmp2);

Однако, если я изменю заявление ITE для tmp2 к следующему

DdNode *tmp2 = Cudd_bddIte(gbm, v2, tmp1, Cudd_ReadLogicZero(gbm));

Я получаю этот неожиданный график:

Для меня это неправильно, так как я ожидаю, что самая верхняя переменная все равно сразу же выдаст 1, если ложь, как на первом рисунке. Что я делаю неправильно?

Answer 1

В (RO)BDD все переменные появляются в определенном порядке. В вашем случае порядок выглядит как "v1, v2, v3", как вы разместили его в этом порядке, и переупорядочение переменных, по-видимому, не произошло.

Функция Cudd_bddIte не требует, чтобы вы соблюдали порядок при создании BDD. Когда вы используете функцию bddIte в своем коде, вы используете эту функциональность: для построения "bdd" вы применяете функцию bddIte к переменной v3, используя два поддеревья над v1 и v2. Тем не менее, v3 находится в конце порядка переменных, поэтому все дерево реструктурируется.

Фактически, второе отображаемое вами дерево обладает ожидаемым свойством: когда v3 имеет значение TRUE, BDD отображает значение переменной в значение TRUE. Это видно из того факта, что единственный способ достичь приемника "0" - через узел 0x2e, который предназначен для переменной v3, а приемник "0" может быть достигнут только тогда, когда выбран преемник узла.