CUDD: Quantification of ZDDs

Question

我正在使用CUDD(https://github.com/ivmai/cudd)使用bdd和zdd功能进行模型检查，我想知道如何通过zdd进行量化。

对于bdd，有函数bddExistAbstract和bddUnivAbstract(请参阅http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddAllDet.html#Cudd_bddUnivAbstract)。

手册中说，函数普遍存在地从bdd中抽象出给定的变量(以封面形式)。我不太明白他们对"；抽象出来"；，因此，我坚持弄清楚量化是如何改变zds的。

你们能帮忙吗？谢谢

Answer 1

Python包dd实现了一个到CUDD的Cython接口，该接口通过量化扩展了CUDD的ZDD函数。例如，在ZDDs:上使用存在量化

from dd import cudd_zdd
zdd = cudd_zdd.ZDD()  # create a ZDD manager
zdd.declare('x', 'y')  # add variables to the manager
u = zdd.add_expr(r'x / y')  # create a BDD `u` for the expression x / y
v = zdd.exist(['y'], u)  # quantify over variable y, i.e., compute E y:  x / y
>>> zdd.to_expr(v)  # convert to an expression as string
'x'

ZDD量化的实现可以在以下位置找到：

https://github.com/tulip-control/dd/blob/24ec9eba335c173e1fe0367a9ac25ec201dee1b5/dd/cudd_zdd.pyx#L1999-L2172

还有许多Python级别的实现也用于开发目的：

https://github.com/tulip-control/dd/blob/24ec9eba335c173e1fe0367a9ac25ec201dee1b5/dd/cudd_zdd.pyx#L1387-L1544

包dd可以从带有pip install dd的PyPI安装。这将在Linux上安装CUDD绑定。在macOS上，CUDD的绑定需要从dd的源代码编译，因此macOS的安装变成：

pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*/
python setup.py install --fetch --cudd --cudd_zdd

如文件README.md.中所述

Answer 2

我准备给出一个长答案，但它可能不会直接帮助您。

TL；DR：据我所知，CUDD没有ExistAbstract或任何类似功能的实现ZDD。但是，我不是CUDD大师，可能忽略了它。

答案很长。您可能只想使用函数。所以我会先报道这个。稍后，我将写一篇关于实现的文章。也许，有人准备添加ZDD到CUDD？

函数bddExistAbstract(Ex)计算给定布尔函数上的存在量化(使用维基百科、youtube、coursera和类似的参考资料来学习所有的数学知识背景)。简而言之，布尔函数F中变量v的存在量化计算为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

布尔函数F中变量v的通用量化计算为Ax(F，v)=F|v=0*F|v=1。

实现ZDD的存在(和通用)量化没有错，但您应该问问自己，你为什么需要它。你用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写的。希望我在进行简化时没有引入错误。请使用我们的公共存储库获取完整且有效的代码(http://svn.savannah.nongnu.org/viewvc/biddy/biddyOp.c?view=markup)，它包括对互补边的支持)

我们将从一个案例开始，其中只请求抽象一个变量。

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,BiddyGetVariable(f))) return f;
}
...
if (biddyManagerType == BIDDYTYPEOBDD) {
if ((fv=BiddyGetVariable(f)) == v) {
r = BiddyOr(MNG,BiddyGetElse(f),BiddyGetThen(f));
}
else {
e = BiddyE(MNG,BiddyGetElse(f),v);
t = BiddyE(MNG,BiddyGetThen(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if ((fv=BiddyGetVariable(f)) == v) {
r = BiddyOr(MNG,BiddyGetElse(f),BiddyGetThen(f));
r = BiddyFoaNode(MNG,v,r,r);
}
else if (BiddyIsSmaller(v,fv)) {
r = BiddyFoaNode(MNG,v,f,f);
}
else {
e = BiddyE(MNG,BiddyGetElse(f),v);
t = BiddyE(MNG,BiddyGetThen(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 = BiddyGetVariable(f);
cv = BiddyGetVariable(cube);
while (!BiddyIsTerminal(cube) && BiddyIsSmaller(cv,fv)) {
cube = BiddyGetThen(cube);
cv = BiddyGetVariable(cube);
}
if (BiddyIsTerminal(cube)) {
return f;
}
if (cv == fv) {
e = BiddyExistAbstract(MNG,BiddyGetElse(f),BiddyGetThen(cube));
t = BiddyExistAbstract(MNG,BiddyGetThen(f),BiddyGetThen(cube));
r = BiddyOr(MNG,e,t);
} else {
e = BiddyExistAbstract(MNG,BiddyGetElse(f),cube);
t = BiddyExistAbstract(MNG,BiddyGetThen(f),cube);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if (BiddyIsTerminal(cube)) {
return f;
}
cv = BiddyGetVariable(cube);
fv = BiddyGetVariable(f);
if (BiddyIsSmaller(cv,fv)) {
r = BiddyExistAbstract(MNG,f,BiddyGetThen(cube));
r = BiddyFoaNode(MNG,cv,r,r);
}
else if (cv == fv) {
e = BiddyExistAbstract(MNG,BiddyGetElse(f),BiddyGetThen(cube));
t = BiddyExistAbstract(MNG,BiddyGetThen(f),BiddyGetThen(cube));
r = BiddyOr(MNG,e,t);
r = BiddyFoaNode(MNG,cv,r,r);
} else {
e = BiddyExistAbstract(MNG,BiddyGetElse(f),cube);
t = BiddyExistAbstract(MNG,BiddyGetThen(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,BiddyGetVariable(f))) return f;
}
...
if (biddyManagerType == BIDDYTYPEOBDD) {
if ((fv=BiddyGetVariable(f)) == v) {
r = BiddyOr(MNG,BiddyGetElse(f),BiddyGetThen(f));
r = BiddyFoaNode(MNG,v,r,biddyZero);
}
else if (BiddyIsSmaller(v,fv)) {
r = BiddyFoaNode(MNG,v,f,biddyZero);
}
else {
e = BiddyElementAbstract(MNG,BiddyGetElse(f),v);
t = BiddyElementAbstract(MNG,BiddyGetThen(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if ((fv=BiddyGetVariable(f)) == v) {
r = BiddyOr(MNG,BiddyGetElse(f),BiddyGetThen(f));
}
else {
e = BiddyElementAbstract(MNG,BiddyGetElse(f),v);
t = BiddyElementAbstract(MNG,BiddyGetThen(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
...
return r;
}