1

问题：如何从使用 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，您可以使用以下代码（基于此出版物）：

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])

输出应该是这样的：

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

0 回答 0