CUDD C ++接口，用于将布尔值转换为BDD以及一组最小项(转换为割集) [英] CUDD C++ Interface for converting Booleans to BDDs and resulting set of minterms (to cutsets)

问题描述

我正在与( https://github.com/ivmai/cudd )一起使用以下重复过程的目标:

I'm working with (https://github.com/ivmai/cudd) with the goal of the following repetitive process:

(1)输入 :(相干，非递减)布尔函数表达式top = a_1 a_2 a_3 ... + x_1 x_2 x_3 ... + z_1 z_2 z_3 ...).我正在使用的布尔型有数千个变量(ai ... zj)和数百个术语.

(1) Input: (Coherent, non-decreasing) Boolean function expression top = a_1a_2a_3...+ x_1x_2x_3... + z_1z_2z_3...). The Booleans I'm working with have thousands of vars (ai...zj) and hundreds of terms.

(2)处理:将布尔值转换为BDD以简化最小项的计算，或者相互转换独家剪辑集(在可靠性"世界中我们称为它们).

(2) Processing: Convert Boolean to a BDD to simplify the calculation of the minterms, or mutually exclusive cut-sets (as we call them in the Reliability world).

(3)输出:取一组中点.最小割据(最小项).通过计算顶部事件概率将(2)中找到的所有最小项相加.

(3) Output: Take the set of m.e. minimal cutsets (minterms). Calculate the top event probability by adding up all the minterms found in (2).

我已经找到了一种使用劳动密集型手动C接口来构建布尔值的方法.我还发现了如何使用出色的tulip-dd Py界面实现此功能，但无法像cudd一样缩放它.

I've found a way to do this with a labor-intensive manual C interface to build the Boolean. I've also found how to do it with the excellent tulip-dd Py interface, but unable to make it scale as with cudd.

现在，我希望使用C ++接口来拥抱我可以两全其美(我要求太多吗?)就是说，说出tulip-dd具有可扩展性的便利性的拥抱.所以这是一些示例代码.我失败的地方是在第3步中，打印出我以前可以在C语言中执行的最小项.如何使用C ++接口来完成它?请查看代码中的注释以了解我的具体想法和尝试.

Now I'm hoping with the C++ interface to cudd I can get the best of both worlds (Am I asking for too much?) Namely, the convenience of say tulip-dd with the scalability of cudd. So here's some sample code. Where I'm failing is in step 3, printing out the minterms, which I used to be able to do in C. How do I do it with the C++ interface?! Please see comments in the code for my specific thoughts and attempts.

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节点.

The CUDD C++ classes are very little more than a wrapper around the "DdManager*" and "DdNode*" data types. They make sure that you don't accidentally forget to Cudd_Ref(..) or Cudd_RecursiveDeref(...) *DD nodes that you are using.

因此，这些类具有可用于访问基础数据类型的函数.因此，例如，如果您想调用"Cudd_PrintDebug"，在顶部"功能BDD，那么您可以执行以下操作:

As such, these classes have functions that you can use to access the underlying data types. So for instance, if you want to call the "Cudd_PrintDebug" function on the "top" BDD, then you can do that with:

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

对代码的修改很小.

请注意，当使用通过"getNode"获取的普通CUDD DdNode *时，功能，您必须手动确保不引入节点计数泄漏.如果您以只读方式"使用DdNode，则仅存储与您还存储的BDD对象相对应的DdNode *，和请确保BDD对象的寿命始终比DdNode *指针长，但这不会发生.我之所以仅提及这一点，是因为在某些时候您可能要遍历BDD的多维数据集.这些本质上是不保证成为最小的最小项.有特殊迭代器在CUDD中.但是，如果您真的想要最小术语，这可能不是正确的方法.还有其他使用CUDD的软件，它带有自己的枚举功能最小项.

Note that when using a plain CUDD DdNode* that you obtain with the "getNode" function, you have to make sure manually that you don't introduce node count leaks. If you use the DdNodes in a "read only fashion", only store DdNode* that correspond to BDD objects that you also store, and make sure that the BDD objects always live longer than the DdNode* pointers, this does not happen, though. I'm only mentioning this since at some point you may want to iterate through the cubes of a BDD. These are essentially not-guaranteed-to-be-minimal minterms. There are special iterators in CUDD for this. However, if you really want the minterms, this may not be right approach. There is other software using CUDD that comes with its own functions for enumerating the minterms.

作为最后的说明(在StackOverflow的范围之外)，您写道:"我正在使用的布尔值具有数千个var(ai ... zj)和数百个术语."-不能保证将BDD与这么多的变量一起使用才是正确的方法.但是请尝试一下.对于基于BDD的方法，具有数千个变量通常是有问题的.您的应用程序可能会也可能不会例外.一种替代方法是将原始表达式的所有最小项的搜索问题编码为增量可满足性(SAT)解决问题.

As a final note (outside of the scope of StackOverflow), you wrote that "The Booleans I'm working with have thousands of vars (ai...zj) and hundreds of terms." - There is no guarantee that using BDDs with so many variables is the way to go here. But please try it out. Having thousands of variables is often problematic for BDD-based approaches. Your application may or may not be an exception to this observation. An alternative approach may be to encode the search problem for all minterms of your original expression as an incremental satisfiability (SAT) solving problem.

这篇关于CUDD C ++接口，用于将布尔值转换为BDD以及一组最小项(转换为割集)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！