0

我正在通过许可指南将产品系列表示为袋模型，其中还考虑了出现的情况以提出 BDD。

我正在尝试将类似的步骤包含在我的问题中。文字说

如果我们采用 bag-model，则实现类似于 set-model 实现，除了处理特征的重复。ROBDD 不允许节点重复。为了处理 BDD 本身中某个特征的出现次数，我们设计了对其进行编码的出现级别。我们对这个数字进行二进制编码。例如，如果我们有一个具有 3 个特征的产品：x、y 和 z，并且一个特征的最大出现次数是 7，那么我们需要三个二进制位对其进行编码。让产品系列 W 有一种产品，它具有三个 x 特征和六个 z 特征以及零个 y 特征。我们的产品系列包含一个产品 Pt，由图 3.7 中的 BDD 表示。代表这个包的 BDD 以类似于集合模型中的方式描述产品。然而，我们对包含 bl、b2 和 b3 的节点级别中的出现进行编码。我们在图 3.7 中读到，如果 x 存在于这个产品中，那么我们必须选择 bl 和 b2，而不是 b3。这是二进制代码 011，分别代表 b3、b2 和 bl，其中 x 出现三个。类似地，对于这个产品中存在的 y，我们得到二进制出现编码为 000，即 0 出现。对于 z，我们得到 110 的二进制出现，它带有数字 6。我们得到二进制出现编码为 000，即 0 次出现。对于 z，我们得到 110 的二进制出现，它带有数字 6。我们得到二进制出现编码为 000，即 0 次出现。对于 z，我们得到 110 的二进制出现，它带有数字 6。

因此，对于产品系列 Z = {{(x,3),(y,0),(z,6)}}，相应的 bdd 将是 ->

BDD

对于产品系列 W = {{(x,3),(y,1),(z,7)}}，BDD 将是

BDD2

但是他是怎么想出这些BDD的，BDD肯定有一些基本的公式。您能否帮助我了解如何为给定的家庭得出相同的公式，以便我可以在其他用例中类似地进一步使用它。谢谢。

4

1 回答 1

0

包是多次出现的元素的集合。动作时间逻辑 (TLA+)Bags中的标准模块包含与袋子相对应的数学定义。

为了将二元决策图的图形转换为公式，我使用了下面的代码。来自 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和dd == 0.5.1（注意：我是它们的作者）。这些在纯 Python 中工作，足以满足这种大小的 BDD（否则构建dd.cudd将允许您使用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 使用否定边表示，本教程中对 BDD进行了解释。

于 2017-11-19T22:31:12.067 回答