Я готов дать длинный ответ, но, вероятно, напрямую вам это не поможет.
TL; DR : Насколько мне известно, в CUDD нет реализации ExistAbstract или любую аналогичную функцию для ZDD. Но я не гуру CUDD и, возможно, пропустил это.
И вот длинный ответ. Вероятно, вы захотите просто использовать функции. Так что сначала я расскажу об этом. Позже напишу о реализации. Может быть, кто-нибудь готов добавить реализацию ZDD в CUDD?
Функция bddExistAbstract (Ex) вычисляет экзистенциальную количественную оценку по заданной логической функции (используйте wikipedia, youtube, coursera и аналогичные ссылки, чтобы изучить всю математическую основу ). Короче говоря, экзистенциальная количественная оценка переменной v в булевой функции F вычисляется как Ex (F, v) = F | v = 0 + F | v = 1. На практике, если вы запишете логическую функцию как формулу суммы произведений, то итоговая формула будет получена простым удалением количественной переменной.
Пример (+ - дизъюнкция, * - конъюнкция, ~ - для отрицания):
F = ~a * c + a * b * ~c + a * ~b * c
Ex(F,b) = ~a * c + a * ~c + a * c = a + c
Универсальная количественная оценка переменной v в булевой функции F вычисляется как Ax (F, v) = F | v = 0 * F | v = 1.
Нет ничего плохого в реализации экзистенциальной (и универсальной) количественной оценки ZDD, но вы должны спросить себя, зачем вам это нужно. Представляете ли вы логические функции (например, функции c) с помощью ZDD? Это не рекомендуется, потому что ZDD кажется неэффективным для этого или, по крайней мере, не более эффективным, чем BDD, просто более сложным. ZDD в основном используются для представления множеств (точнее, «комбинационных множеств»). С наборами экзистенциальная количественная оценка не имеет никакого полезного значения. Например, логическая функция F в предыдущем примере соответствует комбинации наборов {{c}, {a, b}, {b, c}, {a, c}}, в то время как результирующая Ex (F, b) соответствует набору {{ c}, {a, b}, {b, c}, {a, c}, {a}, {a, b, c}}.
Чтобы расширить свой вопрос, наблюдая данный пример, вы может сразу придумать другую функцию, которая дала бы результат для множеств, но в смысле экзистенциальной квантификации для булевой функции. Я назову его ElementAbstract (ElemAbst), и мне неизвестно о его использовании вне моих собственных проектов. Удаляет данный элемент из всех комбинаций. Вот пример:
S = {{c},{a,b},{b,c},{a,c}}
ElemAbst(S,b)= {{c},{a},{c},{a,c}} = {{a},{c},{a,c}}
Теперь поговорим о реализации. Приведу упрощенный код из нашего «пакета Biddy BDD», который написан на C. Надеюсь, я не внес ошибок при выполнении упрощения. Пожалуйста, используйте наш репозиторий publi c для получения полного и рабочего кода (он включает поддержку дополнительных ребер).
Мы начнем со случая, когда требуется абстрагировать только одну переменную.
Biddy_Edge
BiddyE(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
{
Biddy_Edge e, t, r;
Biddy_Variable fv;
...
if (f == biddyZero) return biddyZero;
if (biddyManagerType == BIDDYTYPEOBDD) {
if (BiddyIsSmaller(v,BiddyV(f))) return f;
}
...
if (biddyManagerType == BIDDYTYPEOBDD) {
if ((fv=BiddyV(f)) == v) {
r = BiddyOr(MNG,BiddyE(f),BiddyT(f));
}
else {
e = BiddyE(MNG,BiddyE(f),v);
t = BiddyE(MNG,BiddyT(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if ((fv=BiddyV(f)) == v) {
r = BiddyOr(MNG,BiddyE(f),BiddyT(f));
r = BiddyFoaNode(MNG,v,r,r);
}
else if (BiddyIsSmaller(v,fv)) {
r = BiddyFoaNode(MNG,v,f,f);
}
else {
e = BiddyE(MNG,BiddyE(f),v);
t = BiddyE(MNG,BiddyT(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
...
return r;
}
Более удобно реализовать общий случай, когда сразу абстрагируется множество переменных. Этот вариант включен в CUDD. Переменные, подлежащие абстрагированию, представлены в виде куба, который представляет собой простой продукт всех абстрагируемых переменных. Biddy также включает этот вариант как для BDD, так и для ZDD.
Biddy_Edge
BiddyExistAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube)
{
Biddy_Edge e, t, r;
Biddy_Variable fv,cv;
...
if (f == biddyZero) return biddyZero;
...
if (biddyManagerType == BIDDYTYPEOBDD) {
fv = BiddyV(f);
cv = BiddyV(cube);
while (!BiddyIsTerminal(cube) && BiddyIsSmaller(cv,fv)) {
cube = BiddyT(cube);
cv = BiddyV(cube);
}
if (BiddyIsTerminal(cube)) {
return f;
}
if (cv == fv) {
e = BiddyExistAbstract(MNG,BiddyE(f),BiddyT(cube));
t = BiddyExistAbstract(MNG,BiddyT(f),BiddyT(cube));
r = BiddyOr(MNG,e,t);
} else {
e = BiddyExistAbstract(MNG,BiddyE(f),cube);
t = BiddyExistAbstract(MNG,BiddyT(f),cube);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if (BiddyIsTerminal(cube)) {
return f;
}
cv = BiddyV(cube);
fv = BiddyV(f);
if (BiddyIsSmaller(cv,fv)) {
r = BiddyExistAbstract(MNG,f,BiddyT(cube));
r = BiddyFoaNode(MNG,cv,r,r);
}
else if (cv == fv) {
e = BiddyExistAbstract(MNG,BiddyE(f),BiddyT(cube));
t = BiddyExistAbstract(MNG,BiddyT(f),BiddyT(cube));
r = BiddyOr(MNG,e,t);
r = BiddyFoaNode(MNG,cv,r,r);
} else {
e = BiddyExistAbstract(MNG,BiddyE(f),cube);
t = BiddyExistAbstract(MNG,BiddyT(f),cube);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
...
return r;
}
И, наконец, вот реализация ElementAbstract для абстрагирования одной переменной. Опять же, Biddy поддерживает эту функцию как для BDD, так и для ZDD, не задавая вопросов, полезно ли это кому-то.
Biddy_Edge
BiddyElementAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
{
Biddy_Edge e, t, r;
Biddy_Variable fv;
...
if (f == biddyZero) return biddyZero;
if (biddyManagerType == BIDDYTYPEZBDD) {
if (BiddyIsSmaller(v,BiddyV(f))) return f;
}
...
if (biddyManagerType == BIDDYTYPEOBDD) {
if ((fv=BiddyV(f)) == v) {
r = BiddyOr(MNG,BiddyE(f),BiddyT(f));
r = BiddyFoaNode(MNG,v,r,biddyZero);
}
else if (BiddyIsSmaller(v,fv)) {
r = BiddyFoaNode(MNG,v,f,biddyZero);
}
else {
e = BiddyElementAbstract(MNG,BiddyE(f),v);
t = BiddyElementAbstract(MNG,BiddyT(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if ((fv=BiddyV(f)) == v) {
r = BiddyOr(MNG,BiddyE(f),BiddyT(f));
}
else {
e = BiddyElementAbstract(MNG,BiddyE(f),v);
t = BiddyElementAbstract(MNG,BiddyT(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
...
return r;
}