Как превратить булеву функцию в бинарную диаграмму решений - PullRequest
Новая
       34

Как превратить булеву функцию в бинарную диаграмму решений

0 голосов
/ 30 мая 2018

Скажем, у меня есть следующие логические функции: 

or(x, y) := x || y
and(x, y) := x && y
not(x) := !x
foo(x, y, z) := and(x, or(y, z))
bar(x, y, z, a) := or(foo(x, y, z), not(a))
baz(x, y) := and(x, not(y))

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

Говорят, что булева функция является корневым, направленным ациклическим графом.Имеет несколько нетерминальных и терминальных узлов.Затем он говорит, что каждый нетерминальный узел помечен логической переменной (не функцией), которая имеет два дочерних узла.Я не знаю, что булева переменная из моих определений функций выше.Ребро от узла к дочернему элементу a или b представляет присвоение узла 0 или 1 соответственно.Это называется уменьшено , если изоморфные подграфы были объединены, а узлы, двое детей которых изоморфны, удаляются.Это сокращенная упорядоченная схема принятия двоичных решений (ROBDD).

Исходя из этого и из всех ресурсов, с которыми я столкнулся, я не смог выяснить, как преобразовать эти функции в BDD /ROBDD: 

foo(1, 0, 1)
bar(1, 0, 1, 0)
baz(1, 0)

Или, может быть, это те, которые нужно преобразовать: 

foo(x, y, z)
bar(x, y, z, a)
baz(x, y)

Нужна помощь в объяснении того, что мне нужно сделать, чтобы превратить это в укоренившийсянаправленный ациклический граф.Знание структуры данных также было бы полезно.Кажется, что это именно так: 

var nonterminal = {
  a: child,
  b: child,
  v: some variable, not sure what
}

Но тогда возникает вопрос: как построить граф из этих функций foo, bar и baz.

Ответы [ 2 ]

0 голосов
/ 30 мая 2018

Базовые логические операции AND, OR, XOR и т. Д. Все могут быть вычислены между функциями, которые находятся в представлении BDD, чтобы получить новую функцию в представлении BDD.Алгоритмы для них все аналогичны, за исключением того, как они обрабатывают терминалы, и примерно так:

  • , если результат является терминалом, вернуть этот терминал.
  • , если (op, A, B)кэшируется, возвращает кэшированный результат.

  • различают 3 случая (на самом деле это можно обобщить ..)

    1. A.var == B.var, создайте узел (A.var, OP(A.lo, B.lo), OP(A.hi, B.hi)), где OP представляет рекурсивный вызов этой процедуры.
    2. A.var < B.var, создайте узел (A.var, OP(A.lo, B), OP(A.hi, B))
    3. A.var > B.var, создайте узел (B.var, OP(A, B.lo), OP(A, B.hi))
  • кэшировать результат

«Создать узел», конечно, должен сам себя дедуплицировать, чтобы выполнить «сокращенное» требование.Разделение на 3 случая учитывает требования к упорядочению.

Сложные функции, которые представляют собой дерево простых операций, можно превратить в BDD, применяя это снизу вверх, на каждом шагу только делая простую комбинацию BDD.Это, конечно, имеет тенденцию генерировать узлы, которые не являются частью конечного результата.Переменные и константы имеют тривиальные BDD.

Например, and(x, or(y, z)) создается путем перехода в глубину этого дерева, создания BDD для переменной x (тривиальный узел, (x, 0, 1)), затемдля y и z выполнение OR (пример алгоритма, описанного выше, где только первый шаг действительно заботится о том, чтобы операция была OR) на дисках BDD, которые представляют y и z,и затем выполнение AND для результата, и BDD представляет переменную x.Точный результат зависит от вашего выбора порядка переменных.

Функции, которые оценивают другие функции внутри себя, требуют либо композиции функций (если уже представляют вызываемую функцию с помощью BDD), что возможно с BDD, но имеет некоторые худшие худшиеслучаи или просто встроить определение вызываемой функции.

0 голосов
/ 30 мая 2018

Вы можете сделать это путем оценки всех переменных назначений, например, в случае 

foo(0,0,0) = 0
foo(0,0,1) = 0
foo(0,1,0) = 0
...

Затем создайте график, начните с корня.Каждый аргумент функции получает ребро, помеченное его присваиванием, конечный узел помечается значением результата: 

x0 -0-> y0 -0-> z0 -0-> 0
x0 -0-> y1 -0-> z1 -1-> 0
x0 -0-> y2 -1-> z2 -0-> 0
...

объединяет узлы (y0 = y1 = y2, z0 = z1): 

x0 -0-> y0 -0-> z0 -0-> 0
x0 -0-> y0 -0-> z0 -1-> 0
x0 -0-> y0 -1-> z1 -0-> 0
...

уменьшить количество узлов (есть некоторые правила, которые позволяют объединять узлы или пропускать узлы).Например, поскольку 0 из корня всегда приводит к листу 0, вы можете пропустить последующие решения: 

x0 -0-> 0
...

Обратите внимание, что узлы должны быть помечены именами переменных, которые должны быть назначены наследующие ребра графа.Алгоритм не очень сложен (конечно, существует более эффективный), но я надеюсь, что он визуализирует стратегию.

...