Computing minimal cut sets from Binary Decision Diagram modelled using Python package dd

Question

Question: How to compute the minimal cut sets (MCS) from a Binary Decision Diagram modeled using the Python package dd?

Definition: In a nutshell, and based on the example below, a MCS is that set of minimal and unique occurrences that lead to an output 1.

Example:

Given the binary decision diagram in the picture:

There are just three MCSs:

1. {BE1 & BE2}
2. {BE1 & BE3 & BE4}
3. {BE1 & BE3 & BE5}

Notes:

• A cut set is {BE1 & BE2 & BE3 & BE4}, but it is not minimal, because it is composed by the first and second cut set.
• The cut sets are composed only of those nodes with output 1. Therefore, the MCS is {BE1 & BE3 & BE4} and not {BE1 & ¬BE2 & BE3 & BE4}.

For the BDD you can use the code below (based on this publication):

from dd import autoref

bdd = autoref.BDD()
bdd.declare('BE1','BE2','BE3','BE4','BE5')
# These are the assignments to the input variables
# where the Boolean function is TRUE (the y).
# The assignments where the Boolean function is FALSE
# are not used in the disjunction below.
data = [{'BE1': True, 'BE3': True, 'BE5': True},
 {'BE1': True, 'BE3': True, 'BE4': True},
 {'BE1': True, 'BE3': True, 'BE4': True, 'BE5': True},
 {'BE1': True, 'BE2': True},
 {'BE1': True, 'BE2': True, 'BE5': True},
 {'BE1': True, 'BE2': True, 'BE4': True},
 {'BE1': True, 'BE2': True, 'BE4': True, 'BE5': True},
 {'BE1': True, 'BE2': True, 'BE3': True},
 {'BE1': True, 'BE2': True, 'BE3': True, 'BE5': True},
 {'BE1': True, 'BE2': True, 'BE3': True, 'BE4': True},
 {'BE1': True, 'BE2': True, 'BE3': True, 'BE4': True, 'BE5': True}]

u = bdd.false
for d in data:
    u |= bdd.cube(d)  # disjunction so far
bdd.dump('example.png', roots=[u])

The output should be something like this:

mcs = your_function(bbd)
print(mcs)
[['BE1','BE2'],['BE1','BE3','BE4'],['BE1','BE3','BE5']]