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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку
Вилучено вміст Додано вміст
KoT kB12 (обговорення | внесок)
Створено шляхом перекладу сторінки «Binary decision diagram»
Мітки: перше редагування [вмісту]
(Немає відмінностей)

Версія за 21:00, 5 жовтня 2015

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

Визначення

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

  • Злиття будь-яких ізоморфних підграфів.
  • Ліквідувати будь-яких вузол якого 2 дочірні є ізоморфні.

У більшості випадків під бінарною діаграмою рішень розуміють саме скорочену впорядковану бінарну діаграму рішень (СВБДР). Перевага скороченої впорядкованої БДР в тому, що вона є канонічною (унікальною) для конкретної функції і заданого порядку змінних.  Ця властивість робить СУБДР корисною для перевірки функціональної еквівалентності.[Graph-Based Algorithms for Boolean Function Manipulation, Randal E. Bryant, 1986]

Приклад

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

Історія

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

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

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

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

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

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

Розмір БДР визначається як булевої функцією, так і вибором порядку вхідних змінних. При складанні графа для булевої функції f (x_1, \ ldots, x_ {n}) кількість вузлів в кращому випадку може лінійно залежати від n, а в гіршому випадку залежність може бути експоненційної при невдалому виборі порядку вхідних змінних. Наприклад, дана булева функція f (x_1, \ ldots, x_ {2n}) = x_1x_2 + x_3x_4 + \ cdots + x_ {2n-1} x_ {2n}. Якщо використовувати порядок змінних x_1

BDD for the function ƒ(x1, ..., x8) = x1x2 + x3x4 + x5x6 + x7x8 using bad variable ordering
Good variable ordering

Вибір порядку змінних є критично важливим при використанні таких структур даних на практиці. Проблема знаходження кращого порядку змінних є NP-складним завданням. Більш того, NP-складним є навіть завдання знаходження субоптимального порядку змінних, при якому для будь константи c > 1 розмір БДР не більше ніж в c раз більше оптимального. Однак існують ефективні евристичні методи для вирішення цієї проблеми. Крім того, існують такі функції, для яких розмір графа завжди зростає експоненціально з ростом числа змінних, незалежно від порядку змінних. Це відноситься до функцій множення, що вказує на явну складність факторизації. Дослідження бінарних діаграм рішень привели до появи безлічі суміжних видів графів, таких, як BMD (Binary Moment Diagrams), ZDD (Zero Suppressed Decision Diagram), FDD (Free Binary Decision Diagrams), PDD (Parity decision Diagrams), і MTBDDs (Multiple terminal BDDs).

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

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

кон’юнкція

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

Див. також

Примітки

  1. C. Y. Lee.
  2. Sheldon B. Akers.
  3. Raymond T. Boute, "The Binary Decision Machine as a programmable controller".
  4. Randal E. Bryant.
  5. R. E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293–318.
  6. Karl S. Brace, Richard L. Rudell and Randal E. Bryant.

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

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

Посилання