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:
- {BE1 & BE2}
- {BE1 & BE3 & BE4}
- {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']]
