Бинарная диаграмма решений

Эта статья находится на начальном уровне проработки, в одной из её версий выборочно используется текст из источника, распространяемого под свободной лицензией
Материал из энциклопедии Руниверсалис

Бинарная диаграмма решений (БДР) или программа с ветвлением является формой представления булевой функции [math]\displaystyle{ f(x_1, x_2, ..., x_n) }[/math] от [math]\displaystyle{ n }[/math] переменных в виде направленного ациклического графа, состоящего из внутренних узлов решений (помеченных [math]\displaystyle{ x_i }[/math]), каждый из которых имеет по два потомка, и двух терминальных узлов (помеченных 0 и 1), каждый из которых соответствует одному из двух значений булевой функции. В зарубежной литературе бинарные диаграммы решений и программы с ветвлением называются binary decision diagram (BDD) и branching programs (BP) соответственно.

Определение

Булеву функцию [math]\displaystyle{ f(x_1, x_2, ..., x_n) }[/math] можно представить в виде направленного ациклического графа, состоящего из нескольких внутренних узлов решений и двух терминальных узлов, называемых 0-терминальный узел и 1-терминальный узел. Каждый внутренний узел решений на уровне [math]\displaystyle{ i }[/math] помечен булевой переменной [math]\displaystyle{ x_i }[/math] и имеет по два потомка, называемых младшим потомком и старшим потомком. Переход от внутренного узла [math]\displaystyle{ x_i }[/math] к младшему или старшему потомку выполняется в зависимости от значения переменной [math]\displaystyle{ x_i }[/math] (0 или 1 соответственно). Для заданных значений [math]\displaystyle{ x_1, x_2, ..., x_n }[/math] путь от корневого узла до 1-терминального узла соответствуют тому, что на этих входных значениях булева функция [math]\displaystyle{ f(x_1, x_2, ..., x_n) }[/math] принимает значение 1.

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

БДР называется сокращенной, если для графа применены следующие два правила сокращения:

В большинстве случаев под бинарной диаграммой решений понимают именно сокращенную упорядоченную бинарную диаграмму решений (СУБДР). Преимущество сокращенной упорядоченной БДР в том, что она является канонической (уникальной) для конкретной функции и заданного порядка переменных.[1] Это свойство делает СУБДР полезной для проверки функциональной эквивалентности.

Пример

На рисунке слева изображено бинарное дерево принятия решений (без применения правил сокращения), соответствующее приведенной на этом же рисунке таблице истинности для булевой функции [math]\displaystyle{ f(x_1, x_2, x_3) }[/math]. Для заданных входных значений [math]\displaystyle{ x_1 }[/math], [math]\displaystyle{ x_2 }[/math], [math]\displaystyle{ x_3 }[/math] можно определить значение булевой функции, двигаясь по дереву от корневого узла дерева к терминальным узлам, выбирая направление перехода из узла [math]\displaystyle{ x_i }[/math] в зависимости от входного значения [math]\displaystyle{ x_i }[/math]. Пунктирными линиями на рисунке изображены переходы к младшему потомку, а непрерывными линиями изображены переходы к старшему потомку. Например, если заданы входные значения ([math]\displaystyle{ x_1 = 0 }[/math], [math]\displaystyle{ x_2 = 1 }[/math], [math]\displaystyle{ x_3 = 1 }[/math]), то из корневого узла [math]\displaystyle{ x_1 }[/math] необходимо перейти по пунктирной линии влево (так как значение [math]\displaystyle{ x_1 }[/math] равно 0), после этого необходимо перейти по непрерывным линиям вправо (так как значения [math]\displaystyle{ x_2 }[/math] и [math]\displaystyle{ x_3 }[/math] равны 1). В результате мы окажемся в 1-терминальном узле, то есть значение [math]\displaystyle{ f(x_1 = 0, x_2 = 1, x_3 = 1) }[/math] равно 1.

Бинарное дерево принятия решений на рисунке слева можно преобразовать в бинарную диаграмму решений путём применения двух правил сокращения. Результирующая БДР изображена на рисунке справа.

Бинарное дерево принятия решений, построенное по таблице истинности для функции [math]\displaystyle{ f(x_1, x_2, x_3)=\bar{x_1} \bar{x_2} \bar{x_3} + x_1 x_2 + x_2 x_3 }[/math]
Сокращенная БДР для функции f

История

Основной идеей для создания такой структуры данных послужило разложение Шеннона. Любую булеву функцию по одной из входных переменных можно разделить на две подфункции, называемых положительным и отрицательным дополнением, из которых по принципу if-then-else выбирается только одна подфункция в зависимости от значения входной переменной (по которой выполнялось разложение Шеннона). Представляя каждую такую подфункцию в виде поддерева и продолжая разложение по оставшимся входным переменным, можно получить дерево принятия решений, сокращение которого даст бинарную диаграмму решений. Информация об использовании бинарных диаграмм решений или бинарных ветвящихся программ была впервые опубликована в 1959 году в техническом журнале «Bell Systems Technical Journal»[2][3][4]. БДР под названием каноническая скобочная форма была реализована Мамруковым [5] в САПР для анализа схем, не зависящих от скорости. Потенциал для создания эффективных алгоритмов, основанных на использовании этой структуры данных, исследовал Randal Bryant из университета Карнеги — Меллон: его подход заключался в использовании фиксированного порядка переменных (для однозначности канонического представления каждой булевой функции) и повторного использования общих подграфов (для компактности). Применение этих двух ключевых концепций позволяет повысить эффективность структур данных и алгоритмов для представления множеств и отношений между ними.[6][7] Использование несколькими БДР общих подграфов привело к появлению такой структуры данных, как разделяемая сокращенная упорядоченная бинарная диаграмма решений (Shared Reduced Ordered Binary Decision Diagram).[8] Название БДР теперь в основном используется для этой конкретной структуры данных.

Дональд Кнут в своей видеолекции Fun With Binary Decision Diagrams (BDDs) назвал бинарные диаграммы решений «одной из действительно фундаментальных структур данных, которые появились за последние двадцать пять лет» и отметил, что публикация Randal Bryant от 1986 года[6], осветившая использование бинарных диаграмм решений для манипуляции над булевыми функциями, являлась некоторое время наиболее цитируемой публикацией в компьютерной науке.

Применение

БДР широко используются в системах автоматизированного проектирования (САПР) для синтеза логических схем и в формальной верификации.

В электронике каждая конкретная БДР (даже не сокращенная и не упорядоченная) может быть непосредственно реализована заменой каждого узла на мультиплексор с двумя входами и одним выходом.

Порядок переменных

Размер БДР определяется как булевой функцией, так и выбором порядка входных переменных. При составлении графа для булевой функции [math]\displaystyle{ f(x_1,\ldots, x_{n}) }[/math] количество узлов в лучшем случае может линейно зависеть от [math]\displaystyle{ n }[/math], а в худшем случае зависимость может быть экспоненциальной при неудачном выборе порядка входных переменных. Например, дана булева функция [math]\displaystyle{ f(x_1,\ldots, x_{2n}) = x_1x_2 + x_3x_4 + \cdots + x_{2n-1}x_{2n}. }[/math] Если использовать порядок переменных [math]\displaystyle{ x_1 \lt x_3 \lt \cdots \lt x_{2n-1} \lt x_2 \lt x_4 \lt \cdots \lt x_{2n} }[/math], то понадобится 2n+1 узлов для представления функции в виде БДР. Иллюстрирующая БДР для функции от 8 переменных изображена на рисунке слева. А если использовать порядок [math]\displaystyle{ x_1 \lt x_2 \lt x_3 \lt x_4 \lt \cdots \lt x_{2n-1} \lt x_{2n} }[/math], то можно получить эквивалентную БДР из 2n+2 узлов. Иллюстрирующая БДР для функции от 8 переменных изображена на рисунке справа.

БДР для функции ƒ(x1, …, x8) = x1x2 + x3x4 + x5x6 + x7x8 при использовании неудачного порядка переменных
Аналогичная БДР при удачном выборе порядка переменных

Выбор порядка переменных является критически важным при использовании таких структур данных на практике. Проблема нахождения лучшего порядка переменных является NP-полной задачей.[9] Более того, NP-полной является даже задача нахождения субоптимального порядка переменных, при котором для любой константы c > 1 размер БДР не более чем в c раз больше оптимального.[10] Однако существуют эффективные эвристические методы для решения этой проблемы.

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

Исследования бинарных диаграмм решений привели к появлению множества смежных видов графов, таких, как BMD (Binary Moment Diagrams), ZDD (Zero Suppressed Decision Diagram), FDD (Free Binary Decision Diagrams), PDD (Parity decision Diagrams), и MTBDDs (Multiple terminal BDDs).

Логические операции над бинарными диаграммами решений

Многие логические операции (конъюнкция, дизъюнкция, отрицание) могут быть выполнены непосредственно над БДР с помощью алгоритмов, выполняющих манипуляции над графами за полиномиальное время. Однако повторение этих операций множество раз, например, при формировании конъюнкций или дизъюнкций набора БДР, могут привести к экспоненциально большой БДР в худшем случае. Это происходит из-за того, что результатом любых предшествующих операций над двумя БДР в общем случае может быть БДР с размером, пропорциональным произведению предшествующих размеров, поэтому для нескольких БДР размер может увеличиваться экспоненциально.

См. также

Примечания

  1. ↑ Graph-Based Algorithms for Boolean Function Manipulation, Randal E. Bryant, 1986
  2. ↑ C. Y. Lee. «Representation of Switching Circuits by Binary-Decision Programs». Bell Systems Technical Journal, 38:985-999, 1959.
  3. ↑ Sheldon B. Akers. Binary Decision Diagrams Архивная копия от 7 августа 2007 на Wayback Machine  (недоступная ссылка с 13-05-2013 [4211 дней] — история), IEEE Transactions on Computers, C-27(6):509-516, June 1978.
  4. ↑ Raymond T. Boute, «The Binary Decision Machine as a programmable controller». EUROMICRO Newsletter, Vol. 1(2):16-22, January 1976
  5. ↑ Ю. В. Мамруков, Анализ апериодических схем и асинхронных процессов. Диссертация к.т.н. ЛЭТИ, 1984, 219с.
  6. ↑ 6,0 6,1 Randal E. Bryant. «Graph-Based Algorithms for Boolean Function Manipulation Архивная копия от 23 сентября 2015 на Wayback Machine». IEEE Transactions on Computers, C-35(8):677-691, 1986.
  7. ↑ R. E. Bryant, «Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams» Архивная копия от 23 сентября 2015 на Wayback Machine, ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293—318.
  8. ↑ Karl S. Brace, Richard L. Rudell and Randal E. Bryant. «Efficient Implementation of a BDD Package». In Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990), pages 40-45. IEEE Computer Society Press, 1990.
  9. ↑ Beate Bollig, Ingo Wegener. Improving the Variable Ordering of OBDDs Is NP-Complete, IEEE Transactions on Computers, 45(9):993-1002, September 1996.
  10. ↑ Detlef Sieling. «The nonapproximability of OBDD minimization.» Information and Computation 172, 103—138. 2002.
  • R. Ubar, «Test Generation for Digital Circuits Using Alternative Graphs (in Russian)», in Proc. Tallinn Technical University, 1976, No.409, Tallinn Technical University, Tallinn, Estonia, pp. 75–81.

Рекомендуемая литература

Ссылки

  • ABCD: The ABCD package by Armin Biere, Johannes Kepler Universität, Linz.
  • CMU BDD, BDD package, Carnegie Mellon University, Pittsburgh
  • CUDD: BDD package, University of Colorado, Boulder
  • Installing CUDD in Windows/Visual Studio environments.
  • Biddy: multi-platform academic BDD package, University of Maribor, Slovenia
  • JavaBDD, a Java port of BuDDy that also interfaces to CUDD, CAL, and JDD
  • The Berkeley CAL package which does breadth-first manipulation
  • A. Costa BFunc, includes a BDD boolean logic simplifier supporting up to 32 inputs / 32 outputs (independently)
  • DDD: A C++ library with support for integer valued and hierarchical decision diagrams.
  • JINC: A C++ library developed at University of Bonn, Germany, supporting several BDD variants and multi-threading.
Источник — https://xn--h1ajim.xn--p1ai/index.php?title=Бинарная_диаграмма_решений&oldid=5820985