我正在使用 CUDD ( https://github.com/ivmai/cudd ) 使用 bdd 和 zdd 功能进行模型检查，我想知道如何量化 zdds。
对于 bdd，有 bddExistAbstract 和 bddUnivAbstract 函数（参见http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddAllDet.html#Cudd_bddUnivAbstract）。
该手册说，这些函数普遍地和存在地从 bdd 中抽象出给定的变量（以封面形式）。我不太清楚“抽象出来”是什么意思，因此我坚持弄清楚量化如何改变 zdds。
你们能帮忙吗？谢谢。
Python 包dd实现了到 CUDD 的 Cython 接口，该接口通过量化扩展了 CUDD 的 ZDD 功能。例如，要在 ZDD 上使用存在量化：
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 量化的实现可以在以下位置找到：
并且出于开发目的还存在许多 Python 级别的实现：
该软件包dd可以从PyPI安装，带有pip install dd. 这将在 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中所述。
我准备给出一个很长的答案，但是，它可能不会直接帮助你。
TL;DR：据我所知，CUDD 没有实现 ExistAbstract 或 ZDD 的任何类似功能。但是，我不是 CUDD 大师，可能忽略了它。
这是长答案。您可能只想使用这些功能。所以我将首先介绍这一点。后面我会写实现。也许，有人准备将 ZDD 的实现添加到 CUDD？
函数 bddExistAbstract (Ex) 计算给定布尔函数的存在量化（使用 wikipedia、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}}
现在，让我们谈谈实现。我将给出我们用 C 编写的“Biddy BDD 包”中的简化代码。希望我没有通过执行简化引入错误。请使用我们的公共存储库获取完整且有效的代码（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;
}