Эффективно создавайте структурированную диаграмму бинарных решений

Question

Я пытаюсь создать BDD с определенной структурой. У меня есть одномерная последовательность логических переменных x_i, например x_1, x_2, x_3, x_4, x_5. Мое условие считается выполненным, если нет изолированных единиц или нулей (кроме, возможно, краев).

Я реализовал это с помощью pyeda следующим образом. Условие эквивалентно проверке последовательных троек ([x_1, x_2, x_3]; [x_2, x_3, x_4]; ...) и проверке того, что их значения истинности являются одним из [[1,1,1], [0,0,0], [1,1,0], [0,1,1], [1,0,0], [0,0,1]].

      from functools import reduce
from pyeda.inter import bddvars

def possible_3_grams(farr):
    farr = list(farr)
    poss = [[1,1,1], [0,0,0], [1,1,0], [0,1,1], [1,0,0], [0,0,1]]
    truths = [[farr[i] if p[i] else ~farr[i] for i in range(3)] for p in poss]
    return reduce(lambda x, y: x | y, [reduce(lambda x, y: x & y, t) for t in truths])

X = bddvars('x', k)
Xc = [X[i-1:i+2] for i in range(1,k-1)]
cont_constraints = [possible_3_grams(c) for c in Xc]
cont_constr = reduce(lambda x, y: x & y, cont_constraints)
print(cont_constr.to_dot())

Итоговая диаграмма выглядит так:

Это хорошо работает для коротких последовательностей, но последнее сокращение становится чрезвычайно медленным, когда длина превышает 25. Я бы хотел что-то, что работает для гораздо более длинных последовательностей.

Я подумал, не будет ли в данном случае более эффективным создание BDD напрямую, поскольку проблема имеет много структуры. Однако я не могу найти способ напрямую управлять BDD в pyeda.

Кто-нибудь знает, как я могу заставить это работать более эффективно?

Answer 1

Этот пример можно решить для большого количества переменных с помощью пакета dd, который можно установить с

      pip install dd

Например,

      from functools import reduce

from dd.autoref import BDD


def possible_3_grams(farr):
    farr = list(farr)
    poss = [[1, 1, 1], [0, 0, 0], [1, 1, 0], [0, 1, 1], [1, 0, 0], [0, 0, 1]]
    truths = [[farr[i] if p[i] else ~ farr[i] for i in range(3)] for p in poss]
    return reduce(lambda x, y: x | y, [reduce(lambda x, y: x & y, t) for t in truths])


def main():
    k = 100
    xvars = [f'x{i}' for i in range(k)]
    bdd = BDD()
    bdd.declare(*xvars)
    X = [bdd.add_expr(x) for x in xvars]
    Xc = [X[i-1:i+2] for i in range(1, k-1)]
    cont_constraints = [possible_3_grams(c) for c in Xc]
    cont_constr = reduce(lambda x, y: x & y, cont_constraints)
    print(cont_constr)
    bdd.dump('example.png', [cont_constr])

Вышеупомянутое использует чистую реализацию BDD на Python в модуле dd.autoref. В модуле доступна реализация Cython dd.cudd который взаимодействует с библиотекой CUDD в C.Эту реализацию можно использовать, заменив оператор импорта

      from dd.autoref import BDD

с заявлением

      from dd.cudd import BDD

Приведенный выше сценарий с использованием класса dd.autoref.BDD работает на k = 800(с комментариями к заявлению). Приведенный выше сценарий с использованием класса dd.cudd.BDD работает на k = 10000, при условии, что сначала отключено динамическое переупорядочение bdd.configure(reordering=False), и создает BDD с 39992 узлами (с bdd.dump заявление прокомментировано).

Диаграмма для k = 100 следующее:

Если также интересна минимизация двухуровневой логики, то она реализована в пакете omega, пример можно найти по адресу: https://github.com/tulip-control/omega/blob/master/examples/minimal_formula_from_bdd.py