Создание диаграммы двоичных решений из доступной структуры данных

Этот вопрос довольно длинный; пожалуйста, потерпите меня.

У меня есть структура данных с такими элементами {x1, x2, x3, x4, x5}:

{0 0 0 0 0, 0 0 0 1 0, 1 1 1 1 0,.....}

Они представляют все ИСТИНА в таблице истинности. Конечно, 5-битные строковые элементы, отсутствующие в этом наборе, соответствуют FALSE в таблице истинности. Но у меня нет булевой функции, соответствующей указанной структуре данных набора.

Я вижу этот вопрос, но здесь все ответы предполагают, что задана логическая функция, что неверно.

Мне нужно построить ROBDD, а затем ZDD из данной структуры данных набора. Желательно с доступными пакетами питона, как эти.

Есть совет от экспертов? Я уверен, что в этом направлении сделано немало.

1 ответ

С пакетом Python dd, который можно установить с помощью диспетчера пакетов pip с pip install dd, можно преобразовать набор присвоений переменных, в котором логическая функция TRUE диаграмме бинарных решений.

В следующем примере на Python предполагается, что присвоения, в которых функция TRUE даны как набор строк.

from dd import autoref as _bdd


# assignments where the Boolean function is TRUE
data = {'0 0 0 0 0', '0 0 0 1 0', '1 1 1 1 0'}

# variable names
vrs = [f'x{i}' for i in range(1, 6)]
# convert the assignments to dictionaries
assignments = list()
for e in data:
    tpl = e.split()
    assignment = {k: bool(int(v)) for k, v in zip(vrs, tpl)}
    assignments.append(assignment)

# initialize a BDD manager
bdd = _bdd.BDD()
# declare variables
bdd.declare(*vrs)
# create binary decision diagram
u = bdd.false
for assignment in assignments:
    u |= bdd.cube(assignment)

# to confirm
satisfying_assignments = list(bdd.pick_iter(u))
print(satisfying_assignments)

Для более быстрой реализации BDD и для реализации ZDD с использованием библиотеки C CUDD расширения модуля Cythondd.cudd а также dd.cudd_zdd можно установить следующим образом:

pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*
python setup.py install --fetch --cudd --cudd_zdd

Для этого (небольшого) примера нет практической разницы в скорости между чистым модулем Python. dd.autoref и модуль Cython dd.cudd.

Вышеупомянутая диаграмма двоичного решения (BDD) может быть скопирована в диаграмму двоичного решения с подавлением нуля (ZDD) со следующим кодом:

from dd import _copy
from dd import cudd_zdd


# initialize a ZDD manager
zdd = cudd_zdd.ZDD()
# declare variables
zdd.declare(*vrs)
# copy the BDD to a ZDD
u_zdd = _copy.copy_bdd(u, zdd)

# confirm
satisfying_assignments = list(zdd.pick_iter(u_zdd))
print(satisfying_assignments)

Для установки модуля cudd_zddпожалуйста, скачайте ddпакет из своего репозитория GitHub, потому что этого модуля нет в последней выпущенной версии (v0.5.5) на PyPI.

Другие вопросы по тегам