CUDD: ZDDs的量化

Question

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

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

手册说，函数普遍存在地从bdd中抽象出给定的变量(以封面形式)。我不太明白“抽象出来”是什么意思，因此我坚持要弄清楚量化是如何改变zdd的。

你们能帮上忙吗？谢谢。

Answer 1

Python包dd实现了一个CUDD接口，该接口通过量化扩展了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'

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

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

可以使用pip install dd从PyPI安装dd包。这将在Linux上安装CUDD绑定。在macOS上，需要从dd的源代码编译到CUDD的绑定，因此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或任何类似的ZDDs函数。但是，我不是CUDD大师，可能忽略了这一点。

这是一个很长的答案。您可能只想使用这些函数。因此，我将首先介绍这个。稍后，我将编写有关实现的内容。也许，有人已经准备好将ZDDs的实现添加到CUDD中？

Function 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。

为ZDDs实现存在的(和通用的)量化没有错，但您应该问问自己，为什么需要它。您是否使用ZDDs表示布尔函数(例如，特征函数)？这是不可取的，因为ZDDs在这方面似乎效率不高，或者至少不比BDDs更有效，只是更复杂。ZDDs主要用于表示集合(更准确地说，是“组合集合”)。对于集合，存在量词没有任何有用的意义。例如，上例中的布尔函数F对应于组合集合{{c}，{a，b}，{b，c}，{a，c}}，而得到的Ex(F，b)对应于集合{{c}，{a，b}，{b，c}，{a，c}，{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还包括BDDs和ZDDs的这个变体。

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支持BDDs和ZDDs的这一功能，而不会询问这是否对某人有用。

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