This is probably a question for this forum's resident CUDD/BDD expert, @DCTLib, but if other have insights, welcome of course!
Consider a given minterm such as: 0--0---0--0---0----11 1 .
I need to take each minterm individually and replace "1" with P(x_i) (I'm working with probabilities of the variables), 0 with 1-P(x_i) and "-" with 1. Then I multiple the factors within a minterm, P(x_i)...(1-P(x_j)) and add them all up to obtain the probability of the top event.(A sum-product of probabilities corresponding to the minterms)
The reason I need to take them one by one is that I'm working with large files that blow-up the memory.Once I'm over 80-100 variables, you're in the TB OoM for the whole minterm textfile dump size. I wanted to take each minterm, add it to the running sum and delete it once added, if possible.
Hope this is clear, but if not, might take some iterations. Thanks,
You have a couple of options here:
a) It seems like you already have a text file with output of Cudd_PrintMinterm on a BDD. Computing your sum of the values of the minterms is not actually a CUDD question. Just parse the lines one-by-one and compute the sum on the fly:
std::ifstream inFile("minterms.txt");
std::string currentLine;
double sumSoFar = 0;
while (std::getline(inFile,currentLine)) {
// Process the line "currentLine"
};
if (inFile.fail()) throw "Oopsie";
But you can also do this in python. You may need to work on the numerical accuracy with this approach.
b) The way the problem is described, there is no need to iterate through the minterms, but rather you can assign to each BDD node n a probability p(n), and compute the probability to the root BDD node. The way you do it is by assigning to the TRUE leaf the probability 1, to the FALSE leaf the probability 0, and for each internal node (t,e,x) with TRUE successor t, ELSE successor e, and variable x compute
p(n) = p(t)*p(x) + p(e)*(1-p(x))
Then p(root) is what you are searching for. This approach is more elegant, but requires you to write a (normally recursive) procedure working on the BDD structure itself. There is an example for counting the satisfying assignments available here (using data types that encapsulate CUDDs own types): https://github.com/VerifiableRobotics/slugs/blob/master/src/BFAbstractionLibrary/BFCudd.cpp