如何使用包模型创建包含出现位的 BDD
How to create BDDs with occurence bits involved using bag model
我正在阅读一份许可指南，将产品系列表示为一个包模型，其中还考虑了出现的情况以提出 BDD。
我正在尝试将类似的步骤包含到我的问题中。文字说
If we adopt the bag-model, the implementation is similar to the set-model implementation except for handling the duplications of features.
ROBDDs do not allow duplications of nodes. To handle the number of occurrences of a feature within the BDD itself, we have devised
occurrence levels that encode it. We encode this number binary. For example, if we have a product with 3 features: x, y and z, and the
maximum number of occurrences of a feature is seven, then we need three binary bits to encode it. Let the product family W have one
product with three x features and six z features and zero y features. Our product family contains a product Pt, represented by the BDD
in Figure 3.7. The BDD representing this bag describes the product in a way similar to that in the set model. However, we encode the
occurrences in the levels of nodes containing bl, b2 and b3. We read in Figure 3.7 that, if x exists in this product, then we have to
select bl and b2, but not b3. This is the binary code 011 representing b3, b2 and bl respectively which carries the occurrence of three for
x. Similarly, for y to exist in this product, we get the binary occurrence encoding to be 000 which is 0 occurrences. For z, we get the
binary occurrence of 110 which carries the number six.
因此，对于产品系列 Z = {{(x,3),(y,0),(z,6)}} 相应的 bdd 将是 ->
对于产品系列 W = {{(x,3),(y,1),(z,7)}}，BDD 将是
但是他是怎么想出这些 BDD 的，BDD 一定有一些潜在的公式。您能否帮助我了解如何为给定的家庭得出相同的公式，以便我可以在其他用例中进一步类似地使用它。谢谢
一个bag is a collection of elements with multiple occurrences. The standard module Bags in the Temporal Logic of Actions (TLA+)包含一个对应包的数学定义
为了将 binary decision diagram 的图形转换为公式，我使用了下面的代码。 OP 中第一个 BDD 的答案是：
/\ b \in 0 .. 7
/\ x \in 0 .. 1
/\ y \in 0 .. 1
/\ z \in 0 .. 1
/\ \/ (b = 0) /\ (y = 1)
\/ (b = 3) /\ (x = 1)
\/ (b = 6) /\ (z = 1)
这个表达式是用TLA+写的。
上面实际上不是一个包，因为一个包中每个元素至少出现一次（所以没有出现y意味着这不是一个包；省略 y 应该把它变成一个 BDD 对应一个包）。包包是否适合代表产品系列是另外一个问题，我不会讨论。
您可以调整代码以确认第二张图中显示的 BDD 的公式。
下面的代码使用了 Python 包 omega == 0.1.1 and dd == 0.5.1 (note: I'm an author of them). These work in pure Python, which suffices for BDDs of this size (otherwise building dd.cudd will let you use CUDD——当然这对于小到可以手写的 BDD 来说没有区别。
#!/usr/bin/env python
"""Convert from a BDD figure to a formula."""
from omega.symbolic import fol
# "bare" BDDs (without integers) can be used also
# via the package `dd`
# from dd import autoref as _bdd
# bdd = _bdd.BDD()
ctx = fol.Context()
ctx.declare(x=(0, 1), y=(0, 1), z=(0, 1), b=(0, 7))
bdd = ctx.bdd
# bdd.declare('x', 'y', 'z', 'b1', 'b2', 'b3')
# level of b3
u1 = bdd.add_expr('b_2')
u2 = bdd.add_expr('~ b_2')
# level of b2
u3 = bdd.add_expr(f'ite(b_1, {u1}, FALSE)')
u4 = bdd.add_expr(f'ite(b_1, FALSE, {u2})')
u5 = bdd.add_expr(f'ite(b_1, {u1}, {u2})')
u6 = bdd.add_expr(f'ite(b_1, {u2}, FALSE)')
# level of b1
u7 = bdd.add_expr(f'ite(b_0, FALSE, {u3})')
u8 = bdd.add_expr(f'ite(b_0, FALSE, {u4})')
u9 = bdd.add_expr(f'ite(b_0, FALSE, {u5})')
u10 = bdd.add_expr(f'ite(b_0, {u6}, {u3})')
u11 = bdd.add_expr(f'ite(b_0, {u6}, FALSE)')
u12 = bdd.add_expr(f'ite(b_0, {u6}, {u4})')
u13 = bdd.add_expr(f'ite(b_0, {u6}, {u5})')
# level of z
u14 = bdd.add_expr(f'ite(z_0, {u7}, FALSE)')
u15 = bdd.add_expr(f'ite(z_0, {u9}, {u8})')
u16 = bdd.add_expr(f'ite(z_0, {u10}, {u11})')
u17 = bdd.add_expr(f'ite(z_0, {u13}, {u12})')
# level of y
u18 = bdd.add_expr(f'ite(y_0, {u15}, {u14})')
u19 = bdd.add_expr(f'ite(y_0, {u17}, {u16})')
# level of x
from_fig = bdd.add_expr(f'ite(x_0, {u19}, {u18})')
# the variable order from the first figure in the OP
levels = dict(x_0=0, y_0=1, z_0=2, b_0=3, b_1=4, b_2=5)
fol._bdd.reorder(bdd, levels)
bdd.dump('foo_1.png', [from_fig])
# a better variable order
levels = dict(b_0=0, b_1=1, b_2=2, x_0=3, y_0=4, z_0=5)
fol._bdd.reorder(bdd, levels)
bdd.dump('foo_2.png', [from_fig])
# Create the BDD directly from an expression
s = r'''
\/ (b = 3 /\ x = 1)
\/ (b = 0 /\ y = 1)
\/ (b = 6 /\ z = 1)
'''
from_formula = ctx.add_expr(s)
assert from_formula == from_fig
# print a minimal formula in disjunctive normal form
# use this to covert BDDs to expressions
print(ctx.to_expr(from_fig, show_dom=True))
依赖项可以用pip安装：
pip install dd==0.5.6
pip install omega==0.3.1
通过按照上述代码对变量的级别进行重新排序，我们可以获得更小的 (RO)BDD：
以上BDD用negated edges, which are explained in this tutorial on BDDs表示。
我正在阅读一份许可指南，将产品系列表示为一个包模型，其中还考虑了出现的情况以提出 BDD。
我正在尝试将类似的步骤包含到我的问题中。文字说
If we adopt the bag-model, the implementation is similar to the set-model implementation except for handling the duplications of features. ROBDDs do not allow duplications of nodes. To handle the number of occurrences of a feature within the BDD itself, we have devised occurrence levels that encode it. We encode this number binary. For example, if we have a product with 3 features: x, y and z, and the maximum number of occurrences of a feature is seven, then we need three binary bits to encode it. Let the product family W have one product with three x features and six z features and zero y features. Our product family contains a product Pt, represented by the BDD in Figure 3.7. The BDD representing this bag describes the product in a way similar to that in the set model. However, we encode the occurrences in the levels of nodes containing bl, b2 and b3. We read in Figure 3.7 that, if x exists in this product, then we have to select bl and b2, but not b3. This is the binary code 011 representing b3, b2 and bl respectively which carries the occurrence of three for x. Similarly, for y to exist in this product, we get the binary occurrence encoding to be 000 which is 0 occurrences. For z, we get the binary occurrence of 110 which carries the number six.
因此，对于产品系列 Z = {{(x,3),(y,0),(z,6)}} 相应的 bdd 将是 ->
对于产品系列 W = {{(x,3),(y,1),(z,7)}}，BDD 将是
但是他是怎么想出这些 BDD 的，BDD 一定有一些潜在的公式。您能否帮助我了解如何为给定的家庭得出相同的公式，以便我可以在其他用例中进一步类似地使用它。谢谢
一个bag is a collection of elements with multiple occurrences. The standard module Bags in the Temporal Logic of Actions (TLA+)包含一个对应包的数学定义
为了将 binary decision diagram 的图形转换为公式，我使用了下面的代码。 OP 中第一个 BDD 的答案是：
/\ b \in 0 .. 7
/\ x \in 0 .. 1
/\ y \in 0 .. 1
/\ z \in 0 .. 1
/\ \/ (b = 0) /\ (y = 1)
\/ (b = 3) /\ (x = 1)
\/ (b = 6) /\ (z = 1)
这个表达式是用TLA+写的。
上面实际上不是一个包，因为一个包中每个元素至少出现一次（所以没有出现y意味着这不是一个包；省略 y 应该把它变成一个 BDD 对应一个包）。包包是否适合代表产品系列是另外一个问题，我不会讨论。
您可以调整代码以确认第二张图中显示的 BDD 的公式。
下面的代码使用了 Python 包 omega == 0.1.1 and dd == 0.5.1 (note: I'm an author of them). These work in pure Python, which suffices for BDDs of this size (otherwise building dd.cudd will let you use CUDD——当然这对于小到可以手写的 BDD 来说没有区别。
#!/usr/bin/env python
"""Convert from a BDD figure to a formula."""
from omega.symbolic import fol
# "bare" BDDs (without integers) can be used also
# via the package `dd`
# from dd import autoref as _bdd
# bdd = _bdd.BDD()
ctx = fol.Context()
ctx.declare(x=(0, 1), y=(0, 1), z=(0, 1), b=(0, 7))
bdd = ctx.bdd
# bdd.declare('x', 'y', 'z', 'b1', 'b2', 'b3')
# level of b3
u1 = bdd.add_expr('b_2')
u2 = bdd.add_expr('~ b_2')
# level of b2
u3 = bdd.add_expr(f'ite(b_1, {u1}, FALSE)')
u4 = bdd.add_expr(f'ite(b_1, FALSE, {u2})')
u5 = bdd.add_expr(f'ite(b_1, {u1}, {u2})')
u6 = bdd.add_expr(f'ite(b_1, {u2}, FALSE)')
# level of b1
u7 = bdd.add_expr(f'ite(b_0, FALSE, {u3})')
u8 = bdd.add_expr(f'ite(b_0, FALSE, {u4})')
u9 = bdd.add_expr(f'ite(b_0, FALSE, {u5})')
u10 = bdd.add_expr(f'ite(b_0, {u6}, {u3})')
u11 = bdd.add_expr(f'ite(b_0, {u6}, FALSE)')
u12 = bdd.add_expr(f'ite(b_0, {u6}, {u4})')
u13 = bdd.add_expr(f'ite(b_0, {u6}, {u5})')
# level of z
u14 = bdd.add_expr(f'ite(z_0, {u7}, FALSE)')
u15 = bdd.add_expr(f'ite(z_0, {u9}, {u8})')
u16 = bdd.add_expr(f'ite(z_0, {u10}, {u11})')
u17 = bdd.add_expr(f'ite(z_0, {u13}, {u12})')
# level of y
u18 = bdd.add_expr(f'ite(y_0, {u15}, {u14})')
u19 = bdd.add_expr(f'ite(y_0, {u17}, {u16})')
# level of x
from_fig = bdd.add_expr(f'ite(x_0, {u19}, {u18})')
# the variable order from the first figure in the OP
levels = dict(x_0=0, y_0=1, z_0=2, b_0=3, b_1=4, b_2=5)
fol._bdd.reorder(bdd, levels)
bdd.dump('foo_1.png', [from_fig])
# a better variable order
levels = dict(b_0=0, b_1=1, b_2=2, x_0=3, y_0=4, z_0=5)
fol._bdd.reorder(bdd, levels)
bdd.dump('foo_2.png', [from_fig])
# Create the BDD directly from an expression
s = r'''
\/ (b = 3 /\ x = 1)
\/ (b = 0 /\ y = 1)
\/ (b = 6 /\ z = 1)
'''
from_formula = ctx.add_expr(s)
assert from_formula == from_fig
# print a minimal formula in disjunctive normal form
# use this to covert BDDs to expressions
print(ctx.to_expr(from_fig, show_dom=True))
依赖项可以用pip安装：
pip install dd==0.5.6
pip install omega==0.3.1
通过按照上述代码对变量的级别进行重新排序，我们可以获得更小的 (RO)BDD：
以上BDD用negated edges, which are explained in this tutorial on BDDs表示。