сумка – это набор элементов, которые встречаются несколько раз. Стандартный модуль Bags в разделе Временная логика действий (TLA+) содержит математическое определение, соответствующее сумкам.
Чтобы преобразовать график бинарной диаграммы решений в формулу, я использовал приведенный ниже код. Ответ для первого BDD из OP:
/\ 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('ite(b_1, {u}, False)'.format(u=u1))
u4 = bdd.add_expr('ite(b_1, False, {u})'.format(u=u2))
u5 = bdd.add_expr('ite(b_1, {u1}, {u2})'.format(u1=u1, u2=u2))
u6 = bdd.add_expr('ite(b_1, {u2}, False)'.format(u2=u2))
# level of b1
u7 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
low=u3, high='False'))
u8 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
low=u4, high='False'))
u9 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
low=u5, high='False'))
u10 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
low=u3, high=u6))
u11 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
low='False', high=u6))
u12 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
low=u4, high=u6))
u13 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
low=u5, high=u6))
# level of z
u14 = bdd.add_expr('ite(z_0, {high}, {low})'.format(
low='False', high=u7))
u15 = bdd.add_expr('ite(z_0, {high}, {low})'.format(
low=u8, high=u9))
u16 = bdd.add_expr('ite(z_0, {high}, {low})'.format(
low=u11, high=u10))
u17 = bdd.add_expr('ite(z_0, {high}, {low})'.format(
low=u12, high=u13))
# level of y
u18 = bdd.add_expr('ite(y_0, {high}, {low})'.format(
low=u14, high=u15))
u19 = bdd.add_expr('ite(y_0, {high}, {low})'.format(
low=u16, high=u17))
# level of x
from_fig = bdd.add_expr('ite(x_0, {high}, {low})'.format(
low=u18, high=u19))
# 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 = '''
\/ (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.1
pip install omega==0.1.1
Переупорядочив уровни переменных, как это сделано в приведенном выше коде, мы можем получить меньший (RO)BDD:
Вышеупомянутые BDD представлены с использованием отрицательных ребер. , которые объясняются в этом руководстве по BDD.
person
Ioannis Filippidis
schedule
19.11.2017
