Создание диаграммы двоичных решений из доступной структуры данных
Этот вопрос довольно длинный; пожалуйста, потерпите меня.
У меня есть структура данных с такими элементами {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.