c++ - CUDD C++ 接口(interface)，用于将 bool 值转换为 BDD 和生成的最小项集(到割集)

Question

我正在与 ( https://github.com/ivmai/cudd) 合作，目标是执行以下重复过程:

(1)输入:(相干，非递减) bool 函数表达式顶部 = a_1a_2a_3...+ x_1x_2x_3... + z_1z_2z_3...)。我正在使用的 bool 值有数千个变量 (ai...zj) 和数百个术语。

(2)处理:将Boolean转换为BDD以简化minterms的计算，或者相互独家割集(正如我们在可靠性领域中所称的那样)。

(3) 输出:取m.e.的集合。最小割集(minterms)。计算顶事件概率将 (2) 中找到的所有最小项相加。

我找到了一种方法，使用劳动密集型手动 C 接口(interface)来构建 bool 值。我还找到了如何使用出色的 tulip-dd Py 界面来完成此操作，但无法像使用 cudd 那样进行扩展。

现在我希望通过 C++ 接口(interface)来 cudd 我可以两全其美(我要求太多了吗？)也就是说，说 tulip-dd 的便利性和可扩展性含糖。所以这里有一些示例代码。我失败的地方是第 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 
}

谢谢，桂

Answer 1

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 值有数千个变量 (ai...zj) 和数百个术语。 “- 不能保证使用具有如此多变量的 BDD 是解决问题的方法。但请尝试一下。对于基于 BDD 的方法来说，拥有数千个变量通常是有问题的。您的申请可能会也可能不会异常(exception)。另一种方法可能是将原始表达式的所有最小项的搜索问题编码为增量可满足性 (SAT) 求解问题。