Бинарная диаграмма решений
Бинарная диаграмма решений (БДР) или "программа с ветвлением" является формой представления булевой функции от переменных в виде направленного ациклического графа, состоящего из внутренних узлов решений (помеченных ), каждый из которых имеет по два потомка, и двух терминальных узлов (помеченных 0 и 1), каждый из которых соответствует одному из двух значений булевой функции. В зарубежной литературе бинарные диаграммы решений и программы с ветвлением называются binary decision diagram (BDD) и branching programs (BP) соответственно.
Определение
[править | править код]Булеву функцию можно представить в виде направленного ациклического графа, состоящего из нескольких внутренних узлов решений и двух терминальных узлов, называемых 0-терминальный узел и 1-терминальный узел. Каждый внутренний узел решений на уровне помечен булевой переменной и имеет по два потомка, называемых младшим потомком и старшим потомком. Переход от внутренного узла к младшему или старшему потомку выполняется в зависимости от значения переменной (0 или 1 соответственно). Для заданных значений путь от корневого узла до 1-терминального узла соответствуют тому, что на этих входных значениях булева функция принимает значение 1.
БДР называется упорядоченной, если различные переменные появляются в одном и том же порядке во всех путях от корневого узла графа до одной из терминальных вершин. При этом, некоторые переменные в путях могут отсутствовать, если над графом ранее была произведена операция сокращения.
БДР называется сокращенной, если для графа применены следующие два правила сокращения:
- Слияние любых изоморфных подграфов.
- Удаление всех узлов с изоморфными потомками.
В большинстве случаев под бинарной диаграммой решений понимают именно сокращенную упорядоченную бинарную диаграмму решений (СУБДР). Преимущество сокращенной упорядоченной БДР в том, что она является канонической (уникальной) для конкретной функции и заданного порядка переменных[1]. Это свойство делает СУБДР полезной для проверки функциональной эквивалентности.
Пример
[править | править код]На рисунке слева изображено бинарное дерево принятия решений (без применения правил сокращения), соответствующее приведенной на этом же рисунке таблице истинности для булевой функции . Для заданных входных значений , , можно определить значение булевой функции, двигаясь по дереву от корневого узла дерева к терминальным узлам, выбирая направление перехода из узла в зависимости от входного значения . Пунктирными линиями на рисунке изображены переходы к младшему потомку, а непрерывными линиями изображены переходы к старшему потомку. Например, если заданы входные значения (, , ), то из корневого узла необходимо перейти по пунктирной линии влево (так как значение равно 0), после этого необходимо перейти по непрерывным линиям вправо (так как значения и равны 1). В результате мы окажемся в 1-терминальном узле, то есть значение равно 1.
Бинарное дерево принятия решений на рисунке слева можно преобразовать в бинарную диаграмму решений путём применения двух правил сокращения. Результирующая БДР изображена на рисунке справа.
История
[править | править код]Основной идеей для создания такой структуры данных послужило разложение Шеннона. Любую булеву функцию по одной из входных переменных можно разделить на две подфункции, называемых положительным и отрицательным дополнением, из которых по принципу if-then-else выбирается только одна подфункция в зависимости от значения входной переменной (по которой выполнялось разложение Шеннона). Представляя каждую такую подфункцию в виде поддерева и продолжая разложение по оставшимся входным переменным, можно получить дерево принятия решений, сокращение которого даст бинарную диаграмму решений. Информация об использовании бинарных диаграмм решений или бинарных ветвящихся программ была впервые опубликована в 1959 году в техническом журнале «Bell Systems Technical Journal»[2][3][4]. Потенциал для создания эффективных алгоритмов, основанных на использовании этой структуры данных, исследовал Randal Bryant из университета Карнеги — Меллон: его подход заключался в использовании фиксированного порядка переменных (для однозначности канонического представления каждой булевой функции) и повторного использования общих подграфов (для компактности). Применение этих двух ключевых концепций позволяет повысить эффективность структур данных и алгоритмов для представления множеств и отношений между ними[5][6]. Использование несколькими БДР общих подграфов привело к появлению такой структуры данных, как разделяемая сокращенная упорядоченная бинарная диаграмма решений (Shared Reduced Ordered Binary Decision Diagram)[7]. Название БДР теперь в основном используется для этой конкретной структуры данных.
Дональд Кнут в своей видеолекции Fun With Binary Decision Diagrams (BDDs) назвал бинарные диаграммы решений «одной из действительно фундаментальных структур данных, которые появились за последние двадцать пять лет» и отметил, что публикация Randal Bryant от 1986 года[5], осветившая использование бинарных диаграмм решений для манипуляции над булевыми функциями, являлась некоторое время наиболее цитируемой публикацией в компьютерной науке.
Применение
[править | править код]БДР широко используются в системах автоматизированного проектирования (САПР) для синтеза логических схем и в формальной верификации.
В электронике каждая конкретная БДР (даже не сокращенная и не упорядоченная) может быть непосредственно реализована заменой каждого узла на мультиплексор с двумя входами и одним выходом.
Порядок переменных
[править | править код]Размер БДР определяется как булевой функцией, так и выбором порядка входных переменных. При составлении графа для булевой функции количество узлов в лучшем случае может линейно зависеть от , а в худшем случае зависимость может быть экспоненциальной при неудачном выборе порядка входных переменных. Например, дана булева функция Если использовать порядок переменных , то понадобится 2n+1 узлов для представления функции в виде БДР. Иллюстрирующая БДР для функции от 8 переменных изображена на рисунке слева. А если использовать порядок , то можно получить эквивалентную БДР из 2n+2 узлов. Иллюстрирующая БДР для функции от 8 переменных изображена на рисунке справа.
Выбор порядка переменных является критически важным при использовании таких структур данных на практике. Проблема нахождения лучшего порядка переменных является NP-полной задачей[8]. Более того, NP-полной является даже задача нахождения субоптимального порядка переменных, при котором для любой константы c > 1 размер БДР не более чем в c раз больше оптимального[9]. Однако существуют эффективные эвристические методы для решения этой проблемы.
Кроме того, существуют такие функции, для которых размер графа всегда растет экспоненциально с ростом числа переменных, независимо от порядка переменных. Это относится к функциям умножения, что указывает на явную сложность факторизации.
Исследования бинарных диаграмм решений привели к появлению множества смежных видов графов, таких, как BMD (Binary Moment Diagrams), ZDD (Zero Suppressed Decision Diagram), FDD (Free Binary Decision Diagrams), PDD (Parity decision Diagrams), и MTBDDs (Multiple terminal BDDs).
Логические операции над бинарными диаграммами решений
[править | править код]Многие логические операции (конъюнкция, дизъюнкция, отрицание) могут быть выполнены непосредственно над БДР с помощью алгоритмов, выполняющих манипуляции над графами за полиномиальное время. Однако повторение этих операций множество раз, например, при формировании конъюнкций или дизъюнкций набора БДР, могут привести к экспоненциально большой БДР в худшем случае. Это происходит из-за того, что результатом любых предшествующих операций над двумя БДР в общем случае может быть БДР с размером, пропорциональным произведению предшествующих размеров, поэтому для нескольких БДР размер может увеличиваться экспоненциально.
См. также
[править | править код]Примечания
[править | править код]- ↑ Graph-Based Algorithms for Boolean Function Manipulation, Randal E. Bryant, 1986
- ↑ C. Y. Lee. «Representation of Switching Circuits by Binary-Decision Programs». Bell Systems Technical Journal, 38:985-999, 1959.
- ↑ Sheldon B. Akers. Binary Decision Diagrams Архивная копия от 7 августа 2007 на Wayback Machine (недоступная ссылка с 13-05-2013 [4078 дней] — история), IEEE Transactions on Computers, C-27(6):509-516, June 1978.
- ↑ Raymond T. Boute, «The Binary Decision Machine as a programmable controller». EUROMICRO Newsletter, Vol. 1(2):16-22, January 1976
- ↑ 1 2 Randal E. Bryant. «Graph-Based Algorithms for Boolean Function Manipulation Архивная копия от 23 сентября 2015 на Wayback Machine». IEEE Transactions on Computers, C-35(8):677-691, 1986
- ↑ 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.
- ↑ 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.
- ↑ Beate Bollig, Ingo Wegener. Improving the Variable Ordering of OBDDs Is NP-Complete, IEEE Transactions on Computers, 45(9):993-1002, September 1996.
- ↑ 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.
Рекомендуемая литература
[править | править код]- D. E. Knuth, «The Art of Computer Programming Volume 4, Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams» (Addison-Wesley Professional, March 27, 2009) viii+260pp, ISBN 0-321-58050-8. Draft of Fascicle 1b available for download.
- H. R. Andersen «An Introduction to Binary Decision Diagrams», Lecture Notes, 1999, IT University of Copenhagen.
- Ch. Meinel, T. Theobald, «Algorithms and Data Structures in VLSI-Design: OBDD — Foundations and Applications», Springer-Verlag, Berlin, Heidelberg, New York, 1998. Complete textbook available for download.
- Rüdiger Ebendt; Görschwin Fey; Rolf Drechsler. Advanced BDD optimization (англ.). — Springer[англ.], 2005. — ISBN 978-0-387-25453-1.
- Bernd Becker; Rolf Drechsler. Binary Decision Diagrams: Theory and Implementation (англ.). — Springer[англ.], 1998. — ISBN 978-1-4419-5047-5.
- O. A. Finko, K. S. Meretukov, Systems of Boolean functions: numerical decomposition in Z_m ring, OP&PM Surveys on Applied and Industrial Mathematics. Proceedings II International Baltic Symposium on Applied and Industrial Mathematics (Svetlogorsk, June 12 – 18, 2016), 23, TVP, Moscow, 2016, 167-168.
Ссылки
[править | править код]- 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.