Бінарна діаграма рішень: відмінності між версіями

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


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


Шлях від кореня до 1-терміналу представляє (можливо частково) набори змінних, для яких задана булева функція приймає значення «істина». Як шлях прямує від кореня до нижнього або верхнього нащадка, так і змінна у вузлі ставиться у відповідність 0 або 1.
Шлях від кореня до 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.
На малюнку ліворуч зображене бінарне [[дерево прийняття рішень]] (без застосування правил скорочення), відповідне наведеної на цьому ж малюнку [[таблиці істинності]] для булевої функції <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.


Бінарне дерево прийняття рішень на малюнку ліворуч можна перетворити в бінарну діаграму рішень шляхом застосування двох правил скорочення. БДР, яка буде отримана після скорочення, зображена на малюнку праворуч.
Бінарне дерево прийняття рішень на малюнку ліворуч можна перетворити в бінарну діаграму рішень шляхом застосування двох правил скорочення. БДР, яка буде отримана після скорочення, зображена на малюнку праворуч.
Рядок 24: Рядок 24:
Потенціал для створення ефективних алгоритмів, заснованих на використанні цієї структури даних, досліджував [[Рендел Брайнт]] з [[Університет Карнегі-Меллон|університету Карнегі&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> Назва БДР тепер в основному використовується для цієї конкретної структури даних.
Потенціал для створення ефективних алгоритмів, заснованих на використанні цієї структури даних, досліджував [[Рендел Брайнт]] з [[Університет Карнегі-Меллон|університету Карнегі&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 року, яка пояснила використання бінарних діаграм рішень для маніпуляції над булевими функціями, була деякий час найбільш цитованою публікацією в комп'ютерній науці.
[[Дональд Кнут]] у своїй відеолекції [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 змінних зображена на малюнку праворуч.
Розмір БДР визначається як булевою функцією, так і вибором порядку вхідних змінних. При складанні графа для булевої функції <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"
{| align="center"


Рядок 40: Рядок 40:
|}
|}
Вибір порядку змінних є критично важливим при використанні таких структур даних на практиці. Проблема знаходження найкращого порядку змінних є 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.
Вибір порядку змінних є критично важливим при використанні таких структур даних на практиці. Проблема знаходження найкращого порядку змінних є 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> Однак існують ефективні евристичні методи для вирішення цієї проблеми.
</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]]).
Дослідження бінарних діаграм рішень привели до появи безлічі суміжних видів графів, таких, як BMD ([[Binary Moment Diagrams]]), ZDD ([[Zero Suppressed Decision Diagram]]), FDD ([[Free Binary Decision Diagrams]]), PDD ([[Parity decision Diagrams]]), і MTBDDs ([[Multiple terminal BDDs]]).

Версія за 19:39, 7 березня 2024

Бінарна діаграма рішень (англ. Binary decision diagram) або програма розгалуження — це структура даних в інформатиці, яка використовується для представлення булевої функції. На більш абстрактному рівні, БДР можна розглядати як стиснене представлення множин або відношень. На відміну від інших стиснених представлень, операції виконуються безпосередньо на стислому представлені, тобто без декомпресії. Інші структури даних, які використовуються для представлення булевої функції мають в собі заперечення нормальної формипропозіціональний орієнтований ациклічний граф[en].

Визначення

Булева функція може бути представлена у вигляді орієнтованого ациклічного графа, який складається з декількох вузлів рішень і термінальних вузлів. Існують два типи кінцевих вузлів: 0-термінал і 1-термінал. Кожен вузол рішень позначений булевою (логічною) змінною і має два дочірніх вузли з назвою нижній дочірній та верхній дочірній. Ребро з вузла до нижнього (або верхнього) дочірнього вузла являє собою відповідність нулю (або 1). Така БДР називається «впорядкованою», якщо різні змінні з'являються в тому ж порядку на всіх шляхах від кореня. БДР називають скороченою, якщо наступні два правила вже були застосовані до його графи:

  • Злиті будь-які ізоморфні підграфи.
  • Вилучено будь-який вузол, у якого обидва нащадки ізоморфні.

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

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

Приклад

На малюнку ліворуч зображене бінарне дерево прийняття рішень (без застосування правил скорочення), відповідне наведеної на цьому ж малюнку таблиці істинності для булевої функції . Для заданих вхідних значень , , можна визначити значення логічної функції, рухаючись по дереву від кореневого вузла дерева до термінальних вузлів, вибираючи напрямок переходу з вузла залежно від вхідного значення . Пунктирними лініями на малюнку зображені переходи до молодшого нащадку, а безперервними лініями зображені переходи до старшого нащадку. Наприклад, якщо задано вхідні значення (, , ), то з кореневого вузла необхідно перейти по пунктирній лінії ліворуч (оскільки значення дорівнює 0), після цього необхідно перейти по безперервним лініям праворуч (бо значення та дорівнюють 1). У результаті ми опинимося в 1-термінальному вузлі, тобто значення дорівнює 1.

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

Бінарне дерево рішень та таблиця істинності функції
БДР функції f

Історія

Основною ідеєю для створення такої структури даних послужило розкладання Шеннона. Будь-яку булеву функцію по одній з вхідних змінних можна розділити на дві підфункції, званих позитивним і негативним доповненням, з яких за принципом if-then-else вибирається тільки одна підфункція залежно від значення вхідної змінної (за якою виконувалося розкладання Шеннона). Представляючи кожну таку підфункцію у вигляді піддерева і продовжуючи розкладання по решті вхідних змінних, можна отримати дерево прийняття рішень, скорочення якого дасть бінарну діаграму рішень. Інформація про використання бінарних діаграм рішень або бінарних розгалужених програм була вперше опублікована в 1959 році в технічному журналі «Bell Systems Technical Journal»[2][3][4].

Потенціал для створення ефективних алгоритмів, заснованих на використанні цієї структури даних, досліджував Рендел Брайнт з університету Карнегі — Меллон: його підхід полягав у використанні фіксованого порядку змінних (для однозначності канонічного представлення кожної булевої функції) і повторного використання загальних підграфів (для компактності). Застосування цих двох ключових концепцій дозволяє підвищити ефективність структур даних і алгоритмів для представлення множин і відносин між ними.[5][6] Використання декількома БДР загальних підграфів призвело до появи такої структури даних, як розділювана скорочена впорядкована бінарна діаграма рішень (англ. Shared Reduced Ordered Binary Decision Diagram).[7] Назва БДР тепер в основному використовується для цієї конкретної структури даних.

Дональд Кнут у своїй відеолекції Fun With Binary Decision Diagrams (BDDs) назвав бінарні діаграми рішень «однією з дійсно фундаментальних структур даних, які з'явилися за останні двадцять п'ять років» і зазначив, що публікація Рендела Брайнта 1986 року, яка пояснила використання бінарних діаграм рішень для маніпуляції над булевими функціями, була деякий час найбільш цитованою публікацією в комп'ютерній науці.

Застосування

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

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

Порядок змінних

Розмір БДР визначається як булевою функцією, так і вибором порядку вхідних змінних. При складанні графа для булевої функції кількість вузлів у найкращому випадку може лінійно залежати від , а в найгіршому випадку залежність може бути експоненційною при невдалому виборі порядку вхідних змінних. Наприклад, дана булева функція . Якщо використовувати порядок змінних , то знадобиться 2 n + 1 вузлів для представлення функції у вигляді БДР. Ілюструє БДР для функції від 8 змінних зображена на малюнку зліва. А якщо використовувати порядок , то можна отримати еквівалентну БДР з 2n + 2 вузлів. Ілюстрована БДР для функції від 8 змінних зображена на малюнку праворуч.

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

Вибір порядку змінних є критично важливим при використанні таких структур даних на практиці. Проблема знаходження найкращого порядку змінних є 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).

Логічні операції над БДР

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

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

Див. також

Примітки

  1. Graph-Based Algorithms for Boolean Function Manipulation, Randal E. Bryant, 1986
  2. C. Y. Lee.
  3. Sheldon B. Akers.
  4. Raymond T. Boute, «The Binary Decision Machine as a programmable controller».
  5. Randal E. Bryant.
  6. 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.
  7. Karl S. Brace, Richard L. Rudell and Randal E. Bryant.
  8. Beate Bollig, Ingo Wegener. Improving the Variable Ordering of OBDDs Is NP-Complete, IEEE Transactions on Computers, 45(9):993-1002, September 1996.
  9. Detlef Sieling. «The nonapproximability of OBDD minimization.» Information and Computation 172, 103–138. 2002.

Рекомендована література

  • 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 [Архівовано 12 березня 2016 у Wayback Machine.] 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» [Архівовано 24 вересня 2015 у Wayback Machine.], Springer-Verlag, Berlin, Heidelberg, New York, 1998. Complete textbook available for download.
  • Rüdiger Ebendt; Görschwin Fey; Rolf Drechsler (2005). Advanced BDD optimization. Springer. ISBN 978-0-387-25453-1.
  • Bernd Becker; Rolf Drechsler (1998). Binary Decision Diagrams: Theory and Implementation. Springer. ISBN 978-1-4419-5047-5.

Посилання