CUDD C++ 接口，用于将布尔值转换为 BDD 以及生成的最小项集（到割集）

我正在与 (https://github.com/ivmai/cudd https://github.com/ivmai/cudd），目标是进行以下重复过程：

(1) 输入：（连贯、非递减）布尔函数表达式 顶部 = a_1a_2a_3...+ x_1x_2x_3...+z_1z_2z_3...）。我正在使用的布尔值有 数千个变量 (ai...zj) 和数百个术语。

(2) 处理：将布尔值转换为BDD以简化最小项的计算，或者相互 独家割集（我们在可靠性世界中称之为）。

(3) 输出：拿我的一套。最小割集（minterm）。计算顶部事件概率 将 (2) 中找到的所有小项相加。

我找到了一种方法，使用劳动密集型手动 C 接口来构建布尔值。我还找到了如何使用优秀的 tulip-dd Py 接口来做到这一点，但无法使其像 cudd 那样扩展。

现在我希望通过 cudd 的 C++ 接口我可以两全其美（我的要求是不是太高了？）也就是说，tulip-dd 的便利性和 cudd 的可扩展性。这是一些示例代码。我失败的地方是在第 3 步中，打印出了 minterms，我以前可以在 C 中做到这一点。我如何使用 C++ 接口来做到这一点？我的具体想法和尝试请参见代码中的注释。

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*，and确保 BDD 对象的寿命始终比 DdNode* 指针的寿命长，但这不会发生。 我只是提到这一点，因为在某些时候您可能想要迭代 BDD 的多维数据集。这些本质上是不能保证是最低限度的。有CUDD 中为此提供了特殊迭代器 http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddExtDet.html#Cudd_FirstCube。但是，如果您确实想要最小条款，这可能不是正确的方法。还有其他使用 CUDD 的软件有自己的枚举最小项的功能 https://github.com/VerifiableRobotics/slugs/blob/master/src/BFAbstractionLibrary/BFCuddMintermEnumerator.cpp.

作为最后的说明（超出 StackOverflow 的范围），您写道“我正在使用的布尔值有数千个变量（ai...zj）和数百个术语。" - 不能保证使用具有如此多变量的 BDD 就是正确的方法。但请尝试一下。对于基于 BDD 的方法来说，拥有数千个变量通常会出现问题。您的应用程序可能是例外，也可能不是例外另一种方法可能是将原始表达式的所有小项的搜索问题编码为增量可满足性 (SAT) 求解问题。