c++ - CUDD C++接口(interface)，用于将 bool 值转换为BDD以及最小项的结果集(至割集)

我正在(https://github.com/ivmai/cudd)进行以下重复过程的目标:
(1)输入 :(相干，非递减) bool(boolean) 函数表达式
顶部= a_1a_2a_3 ... + x_1x_2x_3 ... + z_1z_2z_3 ...)。我正在使用的 bool(boolean) 型有
数千个变量(ai ... zj)和数百个术语。
(2)处理:将 bool(boolean) 值转换为BDD以简化最小项的计算，或者相互转换
独家剪辑集(我们在“可靠性”世界中称呼它们)。
(3)输出:取一组最小割据(最小项)。计算最高事件概率
将(2)中找到的所有最小项相加。
我已经找到了一种方法，可以使用劳动密集型的手动C接口(interface)来构建 bool(boolean) 值。我还发现了如何使用出色的tulip-dd Py界面实现此功能，但无法像cudd那样进行缩放。
现在，我希望使用C++接口(interface)来拥抱cudd，我可以兼得两者。(我要求太多吗？)就是说，说出tulip-dd的便捷性和cudd的可扩展性。所以这是一些示例代码。我失败的地方是在第3步中，打印出我以前可以在C中完成的最小项。如何使用C++接口(interface)来完成它？请查看代码中的注释以了解我的具体想法和尝试。

int main()
{


/*DdManager* gbm; /* Global BDD manager. I suppose we do not use this if we use the Cudd type below.*/

/* (1-2) Declare the vars and build the Boolean. Convert Boolean to BDD */

    Cudd mgr(0, 0);
    BDD a = mgr.bddVar();
    BDD b = mgr.bddVar();
    BDD c = mgr.bddVar();
    BDD d = mgr.bddVar();
    BDD e = mgr.bddVar();
    BDD top = a*(b + c + d*e);

/* How to print out the equivalent to below, which prints out all minterms and their relevant vars in C.
But the mgr below has to be a *DManager ? If so, how to convert? */

    Cudd_PrintDebug(mgr, BDD, 2, 4);
    return 0
}

谢谢，
桂

最佳答案

CUDD C++类只不过是围绕“DdManager *”和“DdNode *”数据类型的包装器而已。它们确保您不会意外忘记使用的Cudd_Ref(..)或Cudd_RecursiveDeref(...)* DD节点。
因此，这些类具有可用于访问基础数据类型的函数。因此，例如，如果要在“顶部” BDD上调用“Cudd_PrintDebug”函数，则可以使用以下方法进行操作:

    Cudd_PrintDebug(mgr.getManager(), top.getNode(), 2, 4);

您对代码的修改很少。
请注意，在使用通过“getNode”功能获得的普通CUDD DdNode *时，必须手动确保不引入节点数泄漏。如果您以“只读”方式使用DdNode，则仅存储与您还存储的BDD对象相对应的DdNode *，并确保BDD对象的寿命始终比DdNode *指针长，但这不会发生。
我之所以仅提及这一点，是因为在某些时候您可能要遍历BDD的多维数据集。这些本质上是不能保证最小的最小项。有special iterators in CUDD for this。但是，如果您真的想要最小术语，这可能不是正确的方法。 There is other software using CUDD that comes with its own functions for enumerating the minterms。
作为最后的注释(在StackOverflow的范围之外)，您写道:“我正在使用的 bool(boolean) 值具有数千个var(ai ... zj)和数百个术语。” -不能保证将BDD与这么多的变量一起使用才是正确的选择。但是请尝试一下。对于基于BDD的方法而言，具有数千个变量通常是有问题的。您的应用程序可能会也可能不会异常(exception)。一种替代方法是将原始表达式的所有最小项的搜索问题编码为增量可满足性(SAT)解决问题。

关于c++ - CUDD C++接口(interface)，用于将 bool 值转换为BDD以及最小项的结果集(至割集)，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/62944152/