CUDD C++接口，用于将布尔值转换为BDD和生成的minterm集(转换为割集)

Question

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

(1(输入：(相干，非递减(布尔函数表达式top=a_1a_2a_3…+x_1x_2x_3…+z_1z_2z_3…(数千个vars(ai…zj(和数百个术语。

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

(3(输出：取一组m.e.最小割集(minterms(。通过以下公式计算最高事件概率把(2(中找到的所有minterm加起来。

我已经找到了一种方法，使用劳动密集型的手动C接口来构建Boolean。我还发现了如何使用出色的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 
}

谢谢，桂

Answer 1

CUDD C++类只不过是"；DdManager*"；以及"；DdNode*"；数据类型。它们确保您不会意外忘记使用Cudd_Ref(..(或Cudd_RecuriveDeref(…(*DD节点。

因此，这些类具有可用于访问底层数据类型的函数。例如，如果你想调用；Cudd_PrintDebug"；函数在"；顶部"；BDD，那么你可以用

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

对代码的修改是最小的。

注意，当使用普通CUDD DdNode*时；getNode"函数，您必须手动确保不会引入节点计数泄漏。如果在"；只读时尚"；，只存储与您也存储的BDD对象相对应的DdNode*，和请确保BDD对象始终比DdNode*pointers活得更长，但这不会发生。我之所以提到这一点，是因为在某个时候，您可能想要迭代BDD的多维数据集。这些基本上不能保证是最小的期限。CUDD中有专门的迭代器。然而，如果你真的想要薄荷糖，这可能不是正确的方法。还有其他使用CUDD的软件，它自带枚举minterm的功能。

作为最后一点(在StackOverflow的范围之外(，您写道">与我合作的布尔人有数千个变量(ai…zj(和数百个术语"-不能保证使用具有如此多变量的BDD是实现这一目标的方法。但请尝试一下。对于基于BDD的方法来说，拥有数千个变量往往是个问题。您的申请可能是，也可能不是这一观察结果的例外。另一种方法可能是将原始表达式的所有minterm的搜索问题编码为增量可满足性(SAT(求解问题。