Перегляд вихідного коду сторінки Бінарна діаграма рішень

'''Бінарна діаграма рішень''' ({{lang-en|Binary decision diagram}}) або '''програма розгалуження'''&nbsp;— це [[структура даних]] в [[Інформатика|інформатиці]], яка використовується для представлення [[Булева функція|булевої функції]]. На більш абстрактному рівні, БДР можна розглядати як [[Стиснення даних|стиснене]] представлення [[Множина|множин]] або [[Бінарне відношення|відношень]]. На відміну від інших стиснених представлень, операції виконуються безпосередньо на стислому представлені, тобто без декомпресії. Інші [[структури даних]], які використовуються для представлення [[Булева функція|булевої функції]] мають в собі [[заперечення нормальної форми]],&nbsp; {{Нп|пропозіціональний орієнтований ациклічний граф|||Propositional directed acyclic graph}}.

== Визначення ==
Булева функція може бути представлена у вигляді [[Орієнтований ациклічний граф|орієнтованого ациклічного графа]], який складається з декількох вузлів рішень і термінальних вузлів.&nbsp;Існують два типи кінцевих вузлів: 0-термінал і 1-термінал. Кожен вузол рішень <math>N</math> позначений булевою (логічною) змінною <math>V_N</math> і має два [[Дерево (структура даних)|дочірніх вузли]] з назвою нижній дочірній та верхній дочірній. Ребро з вузла <math>V_N</math> до нижнього (або верхнього) дочірнього вузла являє собою відповідність <math>V_N</math> нулю (або 1). Така БДР називається «впорядкованою», якщо різні змінні з'являються в тому ж порядку на всіх шляхах від кореня. БДР називають скороченою, якщо наступні два правила вже були застосовані до його графу:
* Злиті будь-які [[Ізоморфізм графів|ізоморфні]] підграфи.
* Вилучено будь-який вузол, у якого обидва нащадки ізоморфні.
У більшості випадків під '''бінарною діаграмою рішень''' розуміють саме '''скорочену впорядковану бінарну діаграму рішень''' ('''СВБДР'''). Перевага скороченої впорядкованої БДР в тому, що вона є канонічною (єдиною) для конкретної функції й заданого порядку змінних<ref name="Bryant1986">Graph-Based Algorithms for Boolean Function Manipulation, Randal E. Bryant, 1986</ref>.&nbsp; Ця властивість робить СВБДР корисною для перевірки функціональної еквівалентності.

Шлях від кореня до 1-терміналу представляє (можливо частково) набори змінних, для яких задана булева функція приймає значення «істина». Як шлях прямує від кореня до нижнього або верхнього нащадка, так і змінна у вузлі ставиться у відповідність 0 або 1.

=== Приклад ===
На малюнку ліворуч зображене бінарне [[дерево прийняття рішень]] (без застосування правил скорочення), відповідне наведеної на цьому ж малюнку [[таблиці істинності]] для булевої функції <math>f(x_1, x_2, x_3)</math>. Для заданих вхідних значень <math>x_1</math>, <math>x_2</math>, <math>x_3</math> можна визначити значення логічної функції, рухаючись по дереву від кореневого вузла дерева до термінальних вузлів, вибираючи напрямок переходу з вузла <math>x_i</math> залежно від вхідного значення <math>x_i</math>. Пунктирними лініями на малюнку зображені переходи до молодшого нащадку, а безперервними лініями зображені переходи до старшого нащадку. Наприклад, якщо задано вхідні значення (<math>x_1 = 0</math>, <math>x_2 = 1</math>, <math>x_3 = 1</math>), то з кореневого вузла <math>x_1</math> необхідно перейти по пунктирній лінії ліворуч (оскільки значення <math>x_1</math> дорівнює 0), після цього необхідно перейти по безперервним лініям праворуч (бо значення <math>x_2</math> та <math>x_3</math> дорівнюють 1). У результаті ми опинимося в 1-термінальному вузлі, тобто значення <math>f(x_1 = 0, x_2 = 1, x_3 = 1)</math> дорівнює 1.

Бінарне дерево прийняття рішень на малюнку ліворуч можна перетворити в бінарну діаграму рішень шляхом застосування двох правил скорочення. БДР, яка буде отримана після скорочення, зображена на малюнку праворуч.
{| align="center"
|-
| [[Файл:BDD.png|thumb|546px|Бінарне дерево рішень та [[таблиця істинності]] функції <math>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>]]
| [[Файл:BDD simple.svg|thumb|189px|БДР функції f]]
|}

== Історія ==
Основною ідеєю для створення такої структури даних послужило [[розкладання Шеннона]]. Будь-яку [[Булева функція|булеву функцію]] по одній з вхідних змінних можна розділити на дві підфункції, званих позитивним і негативним доповненням, з яких за принципом if-then-else вибирається тільки одна підфункція залежно від значення вхідної змінної (за якою виконувалося розкладання Шеннона). Представляючи кожну таку підфункцію у вигляді піддерева і продовжуючи розкладання по решті вхідних змінних, можна отримати [[дерево прийняття рішень]], скорочення якого дасть бінарну діаграму рішень. Інформація про використання бінарних діаграм рішень або бінарних розгалужених програм була вперше опублікована в 1959 році в технічному журналі «Bell Systems Technical Journal»<ref name="Lee">C. Y. Lee. </ref><ref name="Akers">Sheldon B. Akers. </ref><ref>Raymond T. Boute, «The Binary Decision Machine as a programmable controller». </ref>.

Потенціал для створення ефективних алгоритмів, заснованих на використанні цієї структури даних, досліджував [[Рендел Брайнт]] з [[Університет Карнегі-Меллон|університету Карнегі&nbsp;— Меллон]]: його підхід полягав у використанні фіксованого порядку змінних (для однозначності канонічного представлення кожної булевої функції) і повторного використання загальних підграфів (для компактності). Застосування цих двох ключових концепцій дозволяє підвищити ефективність структур даних і алгоритмів для представлення множин і відносин між ними.<ref name="Bryant-1986">Randal E. Bryant. </ref><ref name="Bryant-1992">R. E. Bryant, «[http://www.cs.cmu.edu/~bryant/pubdir/acmcs92.ps Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams»] {{Webarchive|url=https://web.archive.org/web/20150923224517/http://www.cs.cmu.edu/~bryant/pubdir/acmcs92.ps |date=23 вересня 2015 }}, ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293—318.</ref> Використання декількома БДР загальних підграфів призвело до появи такої структури даних, як розділювана скорочена впорядкована бінарна діаграма рішень ({{lang-en|Shared Reduced Ordered Binary Decision Diagram}}).<ref name="Brace">Karl S. Brace, Richard L. Rudell and Randal E. Bryant. </ref> Назва БДР тепер в основному використовується для цієї конкретної структури даних.

[[Дональд Кнут]] у своїй відеолекції [https://web.archive.org/web/20111101143950/http://myvideos.stanford.edu/player/slplayer.aspx?coll=ea60314a-53b3-4be2-8552-dcf190ca0c0b&co=18bcd3a8-965a-4a63-a516-a1ad74af1119&o=true Fun With Binary Decision Diagrams (BDDs)] назвав бінарні діаграми рішень «однією з дійсно фундаментальних структур даних, які з'явилися за останні двадцять п'ять років» і зазначив, що публікація [[Рендел Брайнт|Рендела Брайнта]] 1986 року, яка пояснила використання бінарних діаграм рішень для маніпуляції над булевими функціями, була деякий час найбільш цитованою публікацією в комп'ютерній науці.

== Застосування ==
БДР широко використовуються в [[Система автоматизованого проєктування і розрахунку|системах автоматизованого проєктування]] (САПР) для синтезу логічних схем і у [[Формальна верифікація|формальній верифікації]].

В електроніці кожна конкретна БДР (навіть не скорочена і не впорядкована) може бути безпосередньо реалізована заміною кожного вузла на [[мультиплексор]] з двома входами й одним виходом.

== Порядок змінних ==
Розмір БДР визначається як булевою функцією, так і вибором порядку вхідних змінних. При складанні графа для булевої функції <math>f(x_1,\ldots, x_{n})</math> кількість вузлів у найкращому випадку може лінійно залежати від <math>n</math>, а в найгіршому випадку залежність може бути експоненційною при невдалому виборі порядку вхідних змінних. Наприклад, дана булева функція <math>f(x_1,\ldots, x_{2n}) = x_1x_2 + x_3x_4 + \cdots + x_{2n-1}x_{2n}.</math>. Якщо використовувати порядок змінних <math>x_1 < x_3 < \cdots < x_{2n-1} < x_2 < x_4 < \cdots < x_{2n}</math>, то знадобиться 2 <sup> '' n '' + 1 </sup> вузлів для представлення функції у вигляді БДР. Ілюструє БДР для функції від 8 змінних зображена на малюнку зліва. А якщо використовувати порядок <math> x_1 <x_2 <x_3 <x_4 <\cdots <x_{2n-1} <x_{2n} </math>, то можна отримати еквівалентну БДР з 2''n '' + 2 вузлів. Ілюстрована БДР для функції від 8 змінних зображена на малюнку праворуч. 
{| align="center"

| [[Файл:BDD_Variable_Ordering_Bad.svg|thumb|638x638px|БДР для функції ''ƒ''(''x''<sub>1</sub>, …, ''x''<sub>8</sub>) = ''x''<sub>1</sub>''x''<sub>2</sub> + ''x''<sub>3</sub>''x''<sub>4</sub> + ''x''<sub>5</sub>''x''<sub>6</sub> + ''x''<sub>7</sub>''x''<sub>8</sub> при використанні невдалого порядку змінних
]]
| [[Файл:BDD_Variable_Ordering_Good.svg|thumb|435x435px|Аналогічна БДР при вдалому виборі порядку змінних]]
|}
Вибір порядку змінних є критично важливим при використанні таких структур даних на практиці. Проблема знаходження найкращого порядку змінних є NP-складним завданням.<ref name="Bollig">Beate Bollig, Ingo Wegener. [http://dx.doi.org/10.1109/12.537122 Improving the Variable Ordering of OBDDs Is NP-Complete], IEEE Transactions on Computers, 45(9):993-1002, September 1996.
</ref> На додаток, [[NP-складна задача|NP-складним]] є навіть завдання знаходження субоптимального порядку змінних, при якому для будь-якої константи c > 1 розмір БДР не більше ніж в c раз більше оптимального.<ref name="Sieling">Detlef Sieling. «The nonapproximability of OBDD minimization.» Information and Computation 172, 103–138. 2002.</ref> Однак існують ефективні [[Евристичний алгоритм|евристичні методи]] для розв'язання цієї проблеми.

Крім того, існують такі функції, для яких розмір графа завжди зростає експоненціально з ростом числа змінних, незалежно від порядку змінних. Це належить до функцій множення, що вказує на явну складність [[Факторизація|факторизації]].

Дослідження бінарних діаграм рішень привели до появи безлічі суміжних видів графів, таких, як BMD ([[Binary Moment Diagrams]]), ZDD ([[Zero Suppressed Decision Diagram]]), FDD ([[Free Binary Decision Diagrams]]), PDD ([[Parity decision Diagrams]]), і MTBDDs ([[Multiple terminal BDDs]]).

== Логічні операції над БДР ==
Багато [[Логічний сполучник|логічних операцій]] можуть бути виконані безпосередньо над БДР за допомогою алгоритмів, що виконують маніпуляції над графами за поліноміальний час.
* [[кон'юнкція]]
* [[Диз'юнкція (логіка)|диз'юнкція]]
* [[заперечення]]
* екзистенціальна абстракція
* універсальна абстракція
Однак повторення цих операцій безліч разів, наприклад, при формуванні кон'юнкцій або диз'юнкцій набору БДР, можуть призвести до експоненціально великого БДР в гіршому випадку. Це відбувається через те, що результатом будь-яких попередніх операцій над двома БДР в загальному випадку може бути БДР з розміром, пропорційним добутку попередніх розмірів, тому для декількох БДР розмір може збільшуватися експоненціально.

== Див. також ==
* [[Задача здійсненності бульових формул]]
* [[Булева алгебра|Булева Алгебра]]

== Примітки ==
{{примітки}}

== Рекомендована література ==
* 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. [http://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz Draft of Fascicle 1b] {{Webarchive|url=https://web.archive.org/web/20160312073634/http://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz |date=12 березня 2016 }} available for download.
* H. R. Andersen «[https://web.archive.org/web/20140222052815/http://configit.com/configit_wordpress/wp-content/uploads/2013/07/bdd-eap.pdf An Introduction to Binary Decision Diagrams,]» Lecture Notes, 1999, IT University of Copenhagen.
* Ch. Meinel, T. Theobald, «[http://www.hpi.uni-potsdam.de/fileadmin/hpi/FG_ITS/books/OBDD-Book.pdf Algorithms and Data Structures in VLSI-Design: OBDD&nbsp;— Foundations and Applications»] {{Webarchive|url=https://web.archive.org/web/20150924032436/http://www.hpi.uni-potsdam.de/fileadmin/hpi/FG_ITS/books/OBDD-Book.pdf |date=24 вересня 2015 }}, Springer-Verlag, Berlin, Heidelberg, New York, 1998. Complete textbook available for download.
* {{Cite book|author1 = Rüdiger Ebendt|author2 = Görschwin Fey|author3 = Rolf Drechsler|title = Advanced BDD optimization|year = 2005|publisher = Springer|isbn = 978-0-387-25453-1}}
* {{Cite book|author1 = Bernd Becker|author2 = Rolf Drechsler|title = Binary Decision Diagrams: Theory and Implementation|year = 1998|publisher = Springer|isbn = 978-1-4419-5047-5}}

== Посилання ==
* [http://fmv.jku.at/abcd/ ABCD] {{Webarchive|url=https://web.archive.org/web/20201024114212/http://fmv.jku.at/abcd/ |date=24 жовтня 2020 }}: The ABCD package by Armin Biere, Johannes Kepler Universität, Linz.
* [http://www-2.cs.cmu.edu/~modelcheck/bdd.html CMU BDD] {{Webarchive|url=https://web.archive.org/web/20110926232927/http://www-2.cs.cmu.edu/~modelcheck/bdd.html |date=26 вересня 2011 }}, BDD package, Carnegie Mellon University, Pittsburgh
* [https://web.archive.org/web/20080603164118/http://vlsi.colorado.edu/~fabio/CUDD/ CUDD]: BDD package, University of Colorado, Boulder
* [https://web.archive.org/web/20120614204152/http://www.technical-recipes.com/category/binary-decision-diagrams/ Installing CUDD in Windows/Visual Studio environments.]
* [http://lms.uni-mb.si/biddy/ Biddy] {{Webarchive|url=https://web.archive.org/web/20151006021204/http://lms.uni-mb.si/biddy/ |date=6 жовтня 2015 }}: multi-platform academic BDD package, University of Maribor, Slovenia
* [http://javabdd.sourceforge.net JavaBDD] {{Webarchive|url=https://web.archive.org/web/20200422142520/http://javabdd.sourceforge.net/ |date=22 квітня 2020 }}, a Java port of BuDDy that also interfaces to CUDD, CAL, and JDD
* The Berkeley [https://web.archive.org/web/20140223023856/http://embedded.eecs.berkeley.edu/Research/cal_bdd/ CAL] package which does breadth-first manipulation
* A. Costa [http://www.dei.isep.ipp.pt/~acc/bfunc/ BFunc] {{Webarchive|url=https://web.archive.org/web/20120712042144/http://www.dei.isep.ipp.pt/~acc/bfunc/ |date=12 липня 2012 }}, includes a BDD boolean logic simplifier supporting up to 32 inputs / 32 outputs (independently)
* [http://ddd.lip6.fr DDD] {{Webarchive|url=https://web.archive.org/web/20170709174244/http://ddd.lip6.fr/ |date=9 липня 2017 }}: A C++ library with support for integer valued and hierarchical decision diagrams.
* [https://archive.today/20130105201510/http://www.jossowski.de/projects/jinc/jinc.html JINC]: A C++ library developed at University of Bonn, Germany, supporting several BDD variants and multi-threading.

{{бібліоінформація}}
{{Структури даних}}

[[Категорія:Булева алгебра]]
[[Категорія:Діаграми]]
[[Категорія:Графи (структури даних)]]