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

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

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

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

• Слияние любых изоморфных подграфов.
• Удаление всех узлов с изоморфными потомками.

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

Пример

На рисунке слева изображено бинарное дерево принятия решений (без применения правил сокращения), соответствующее приведенной на этом же рисунке таблице истинности для булевой функции ${\displaystyle f(x_{1},x_{2},x_{3})}$. Для заданных входных значений ${\displaystyle x_{1}}$, ${\displaystyle x_{2}}$, ${\displaystyle x_{3}}$ можно определить значение булевой функции, двигаясь по дереву от корневого узла дерева к терминальным узлам, выбирая направление перехода из узла ${\displaystyle x_{i}}$ в зависимости от входного значения ${\displaystyle x_{i}}$. Пунктирными линиями на рисунке изображены переходы к младшему потомку, а непрерывными линиями изображены переходы к старшему потомку. Например, если заданы входные значения (${\displaystyle x_{1}=0}$, ${\displaystyle x_{2}=1}$, ${\displaystyle x_{3}=1}$), то из корневого узла ${\displaystyle x_{1}}$ необходимо перейти по пунктирной линии влево (так как значение ${\displaystyle x_{1}}$ равно 0), после этого необходимо перейти по непрерывным линиям вправо (так как значения ${\displaystyle x_{2}}$ и ${\displaystyle x_{3}}$ равны 1). В результате мы окажемся в 1-терминальном узле, то есть значение ${\displaystyle f(x_{1}=0,x_{2}=1,x_{3}=1)}$ равно 1.

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

Бинарное дерево принятия решений, построенное по таблице истинности для функции ${\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}}$

Сокращенная БДР для функции 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], осветившая использование бинарных диаграмм решений для манипуляции над булевыми функциями, являлась некоторое время наиболее цитируемой публикацией в компьютерной науке.

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

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

Размер БДР определяется как булевой функцией, так и выбором порядка входных переменных. При составлении графа для булевой функции ${\displaystyle f(x_{1},\ldots ,x_{n})}$ количество узлов в лучшем случае может линейно зависеть от ${\displaystyle n}$, а в худшем случае зависимость может быть экспоненциальной при неудачном выборе порядка входных переменных. Например, дана булева функция ${\displaystyle f(x_{1},\ldots ,x_{2n})=x_{1}x_{2}+x_{3}x_{4}+\cdots +x_{2n-1}x_{2n}.}$ Если использовать порядок переменных ${\displaystyle x_{1}<x_{3}<\cdots <x_{2n-1}<x_{2}<x_{4}<\cdots <x_{2n}}$, то понадобится 2ⁿ⁺¹ узлов для представления функции в виде БДР. Иллюстрирующая БДР для функции от 8 переменных изображена на рисунке слева. А если использовать порядок ${\displaystyle x_{1}<x_{2}<x_{3}<x_{4}<\cdots <x_{2n-1}<x_{2n}}$, то можно получить эквивалентную БДР из 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).

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

• Задача выполнимости булевых формул
• Булева алгебра

• 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.

• 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.