从使用 Python 包 dd 建模的二元决策图中计算最小割集

如何解决从使用 Python 包 dd 建模的二元决策图中计算最小割集

问题：如何从使用 Python 包 dd 建模的二元决策图中计算最小割集 (MCS)？

定义： 简而言之，根据下面的示例，MCS 是导致输出 1 的最少且唯一的事件集。

示例：

给定图中的二元决策图：

只有三个 MCS：

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

注意事项：

• 一个割集是 {BE1 & BE2 & BE3 & BE4}，但它不是最小的，因为它是由第一个和第二个割集组成的。
• 割集仅由输出为 1 的节点组成。因此，MCS 是 {BE1 & BE3 & BE4} 而不是 {BE1 & ¬BE2 & BE3 & BE4}。

对于 BDD，您可以使用以下代码（基于 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,'BE4': True},'BE4': True,'BE2': True},'BE2': True,'BE3': True},'BE5': True}]

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

输出应该是这样的：

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