www.wikidata.uk-ua.nina.az

Бінарна діаграма рішень англ Binary decision diagram або програма розгалуження це структура даних в інформатиці яка вико

Бінарна діаграма рішень

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

Визначення ред.

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

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

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

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

Приклад ред.

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

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

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

Історія ред.

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

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

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

Застосування ред.

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

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

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

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

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

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

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

Посилання ред.

  • ABCD [ 24 жовтня 2020 у Wayback Machine.]: The ABCD package by Armin Biere, Johannes Kepler Universität, Linz.
  • CMU BDD [ 26 вересня 2011 у Wayback Machine.], BDD package, Carnegie Mellon University, Pittsburgh
  • : BDD package, University of Colorado, Boulder
  • Biddy [ 6 жовтня 2015 у Wayback Machine.]: multi-platform academic BDD package, University of Maribor, Slovenia
  • JavaBDD [ 22 квітня 2020 у Wayback Machine.], a Java port of BuDDy that also interfaces to CUDD, CAL, and JDD
  • The Berkeley package which does breadth-first manipulation
  • A. Costa BFunc [ 12 липня 2012 у Wayback Machine.], includes a BDD boolean logic simplifier supporting up to 32 inputs / 32 outputs (independently)
  • DDD [ 9 липня 2017 у Wayback Machine.]: 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.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри
Дата публікації:
Binarna diagrama rishen angl Binary decision diagram abo programa rozgaluzhennya ce struktura danih v informatici yaka vikoristovuyetsya dlya predstavlennya bulevoyi funkciyi Na bilsh abstraktnomu rivni BDR mozhna rozglyadati yak stisnene predstavlennya mnozhin abo vidnoshen Na vidminu vid inshih stisnenih predstavlen operaciyi vikonuyutsya bezposeredno na stislomu predstavleni tobto bez dekompresiyi Inshi strukturi danih yaki vikoristovuyutsya dlya predstavlennya bulevoyi funkciyi vklyuchayut v sebe zaperechennya normalnoyi formi propozicionalnij oriyentovanij aciklichnij graf en Zmist 1 Viznachennya 1 1 Priklad 2 Istoriya 3 Zastosuvannya 4 Poryadok zminnih 5 Logichni operaciyi nad BDR 6 Div takozh 7 Primitki 8 Rekomendovana literatura 9 PosilannyaViznachennya red Buleva funkciya mozhe buti predstavlena u viglyadi oriyentovanogo aciklichnogo grafa yakij skladayetsya z dekilkoh vuzliv rishen i terminalnih vuzliv Isnuyut dva tipi kincevih vuzliv 0 terminal i 1 terminal Kozhen vuzol rishen N displaystyle N nbsp poznachenij bulevoyu logichnoyu zminnoyu V N displaystyle V N nbsp i maye dva dochirnih vuzli z nazvoyu nizhnij dochirnij ta verhnij dochirnij Rebro z vuzla V N displaystyle V N nbsp do nizhnogo abo verhnogo dochirnogo vuzla yavlyaye soboyu vidpovidnist V N displaystyle V N nbsp nulyu abo 1 Taka BDR nazivayetsya vporyadkovanoyu yaksho rizni zminni z yavlyayutsya v tomu zh poryadku na vsih shlyahah vid korenya BDR nazivayut skorochenoyu yaksho nastupni dva pravila vzhe buli zastosovani do jogo grafu Zliti bud yaki izomorfni pidgrafi Vilucheno bud yakij vuzol u yakogo obidva nashadki izomorfni U bilshosti vipadkiv pid binarnoyu diagramoyu rishen rozumiyut same skorochenu vporyadkovanu binarnu diagramu rishen SVBDR Perevaga skorochenoyi vporyadkovanoyi BDR v tomu sho vona ye kanonichnoyu yedinoyu dlya konkretnoyi funkciyi i zadanogo poryadku zminnih 1 Cya vlastivist robit SUBDR korisnoyu dlya perevirki funkcionalnoyi ekvivalentnosti Shlyah vid korenya do 1 terminalu predstavlyaye mozhlivo chastkovo nabori zminnih dlya yakih zadana buleva funkciya prijmaye znachennya istina Yak shlyah pryamuye vid korenya do nizhnogo abo verhnogo nashadka tak i zminna u vuzli stavitsya u vidpovidnist 0 abo 1 Priklad red Na malyunku livoruch zobrazhene binarne derevo prijnyattya rishen bez zastosuvannya pravil skorochennya vidpovidne navedenoyi na comu zh malyunku tablici istinnosti dlya bulevoyi funkciyi f x 1 x 2 x 3 displaystyle f x 1 x 2 x 3 nbsp Dlya zadanih vhidnih znachen x 1 displaystyle x 1 nbsp x 2 displaystyle x 2 nbsp x 3 displaystyle x 3 nbsp mozhna viznachiti znachennya logichnoyi funkciyi ruhayuchis po derevu vid korenevogo vuzla dereva do terminalnih vuzliv vibirayuchi napryamok perehodu z vuzla x i displaystyle x i nbsp zalezhno vid vhidnogo znachennya x i displaystyle x i nbsp Punktirnimi liniyami na malyunku zobrazheni perehodi do molodshogo nashadku a bezperervnimi liniyami zobrazheni perehodi do starshogo nashadku Napriklad yaksho zadano vhidni znachennya x 1 0 displaystyle x 1 0 nbsp x 2 1 displaystyle x 2 1 nbsp x 3 1 displaystyle x 3 1 nbsp to z korenevogo vuzla x 1 displaystyle x 1 nbsp neobhidno perejti po punktirnij liniyi livoruch oskilki znachennya x 1 displaystyle x 1 nbsp dorivnyuye 0 pislya cogo neobhidno perejti po bezperervnim liniyam pravoruch tak yak znachennya x 2 displaystyle x 2 nbsp ta x 3 displaystyle x 3 nbsp dorivnyuyut 1 U rezultati mi opinimosya v 1 terminalnomu vuzli tobto znachennya f x 1 0 x 2 1 x 3 1 displaystyle f x 1 0 x 2 1 x 3 1 nbsp dorivnyuye 1 Binarne derevo prijnyattya rishen na malyunku livoruch mozhna peretvoriti v binarnu diagramu rishen shlyahom zastosuvannya dvoh pravil skorochennya BDR yaka bude otrimana pislya skorochennya zobrazhena na malyunku pravoruch nbsp Binarne derevo rishen ta tablicya istinnosti funkciyi f x 1 x 2 x 3 x 1 x 2 x 3 x 1 x 2 x 2 x 3 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 nbsp nbsp BDR funkciyi fIstoriya red Osnovnoyu ideyeyu dlya stvorennya takoyi strukturi danih posluzhilo rozkladannya Shennona Bud yaku bulevu funkciyu po odnij z vhidnih zminnih mozhna rozdiliti na dvi pidfunkciyi zvanih pozitivnim i negativnim dopovnennyam z yakih za principom if then else vibirayetsya tilki odna pidfunkciya zalezhno vid znachennya vhidnoyi zminnoyi za yakoyu vikonuvalosya rozkladannya Shennona Predstavlyayuchi kozhnu taku pidfunkciyu u viglyadi piddereva i prodovzhuyuchi rozkladannya po reshti vhidnih zminnih mozhna otrimati derevo prijnyattya rishen skorochennya yakogo dast binarnu diagramu rishen Informaciya pro vikoristannya binarnih diagram rishen abo binarnih rozgaluzhenih program bula vpershe opublikovana v 1959 roci v tehnichnomu zhurnali Bell Systems Technical Journal 2 3 4 Potencial dlya stvorennya efektivnih algoritmiv zasnovanih na vikoristanni ciyeyi strukturi danih doslidzhuvav Randal Bryant z universitetu Karnegi Mellon jogo pidhid polyagav u vikoristanni fiksovanogo poryadku zminnih dlya odnoznachnosti kanonichnogo predstavlennya kozhnoyi bulevoyi funkciyi i povtornogo vikoristannya zagalnih pidgrafiv dlya kompaktnosti Zastosuvannya cih dvoh klyuchovih koncepcij dozvolyaye pidvishiti efektivnist struktur danih i algoritmiv dlya predstavlennya mnozhin i vidnosin mizh nimi 5 6 Vikoristannya dekilkoma BDR zagalnih pidgrafiv prizvelo do poyavi takoyi strukturi danih yak rozdilyuvana skorochena vporyadkovana binarna diagrama rishen Shared Reduced Ordered Binary Decision Diagram yi 7 Nazva BDR teper v osnovnomu vikoristovuyetsya dlya ciyeyi konkretnoyi strukturi danih Donald Knut v svoyij videolekciyi Fun With Binary Decision Diagrams BDDs nazvav binarni diagrami rishen odniyeyu z dijsno fundamentalnih struktur danih yaki z yavilisya za ostanni dvadcyat p yat rokiv i zaznachiv sho publikaciya Randal Bryant vid 1986 yaka osvitila vikoristannya binarnih diagram rishen dlya manipulyaciyi nad bulevimi funkciyami bula deyakij chas najbilsh citovanoyu publikaciyeyu v komp yuternij nauci Zastosuvannya red BDR shiroko vikoristovuyutsya v sistemah avtomatizovanogo proektuvannya SAPR dlya sintezu logichnih shem i u formalnij verifikaciyi V elektronici kozhna konkretna BDR navit ne skorochena i ne vporyadkovana mozhe buti bezposeredno realizovana zaminoyu kozhnogo vuzla na multipleksor z dvoma vhodami i odnim vihodom Poryadok zminnih red Rozmir BDR viznachayetsya yak bulevoyi funkciyeyu tak i viborom poryadku vhidnih zminnih Pri skladanni grafa dlya bulevoyi funkciyi f x 1 x n displaystyle f x 1 ldots x n nbsp kilkist vuzliv u najkrashomu vipadku mozhe linijno zalezhati vid n displaystyle n nbsp a v najgirshomu vipadku zalezhnist mozhe buti eksponencijnoyu pri nevdalomu vibori poryadku vhidnih zminnih Napriklad dana buleva funkciya f x 1 x 2 n x 1 x 2 x 3 x 4 x 2 n 1 x 2 n displaystyle f x 1 ldots x 2n x 1 x 2 x 3 x 4 cdots x 2n 1 x 2n nbsp Yaksho vikoristovuvati poryadok zminnih x 1 lt x 3 lt lt x 2 n 1 lt x 2 lt x 4 lt lt x 2 n displaystyle x 1 lt x 3 lt cdots lt x 2n 1 lt x 2 lt x 4 lt cdots lt x 2n nbsp to znadobitsya 2 n 1 vuzliv dlya predstavlennya funkciyi u viglyadi BDR Ilyustruye BDR dlya funkciyi vid 8 zminnih zobrazhena na malyunku zliva A yaksho vikoristovuvati poryadok x 1 lt x 2 lt x 3 lt x 4 lt lt x 2 n 1 lt x 2 n displaystyle x 1 lt x 2 lt x 3 lt x 4 lt cdots lt x 2n 1 lt x 2n nbsp to mozhna otrimati ekvivalentnu BDR z 2n 2 vuzliv Ilyustrovana BDR dlya funkciyi vid 8 zminnih zobrazhena na malyunku pravoruch nbsp BDR dlya funkciyi ƒ x1 x8 x1x2 x3x4 x5x6 x7x8 pri vikoristanni nevdalogo poryadku zminnih nbsp Analogichna BDR pri vdalomu vibori poryadku zminnihVibir poryadku zminnih ye kritichno vazhlivim pri vikoristanni takih struktur danih na praktici Problema znahodzhennya najkrashogo poryadku zminnih ye NP skladnim zavdannyam 8 Bilsh togo NP skladnim ye navit zavdannya znahodzhennya suboptimalnogo poryadku zminnih pri yakomu dlya bud konstanti c gt 1 rozmir BDR ne bilshe nizh v c raz bilshe optimalnogo 9 Odnak isnuyut efektivni evristichni metodi dlya virishennya ciyeyi problemi Krim togo isnuyut taki funkciyi dlya yakih rozmir grafa zavzhdi zrostaye eksponencialno z rostom chisla zminnih nezalezhno vid poryadku zminnih Ce vidnositsya do funkcij mnozhennya sho vkazuye na yavnu skladnist faktorizaciyi Doslidzhennya binarnih diagram rishen priveli do poyavi bezlichi sumizhnih vidiv grafiv takih yak BMD Binary Moment Diagrams ZDD Zero Suppressed Decision Diagram FDD Free Binary Decision Diagrams PDD Parity decision Diagrams i MTBDDs Multiple terminal BDDs Logichni operaciyi nad BDR red Bagato logichnih operacij mozhut buti vikonani bezposeredno nad BDR za dopomogoyu algoritmiv sho vikonuyut manipulyaciyi nad grafami za polinomialnij chas kon yunkciya diz yunkciya zaperechennya ekzistencialna abstrakciya universalna abstrakciyaOdnak povtorennya cih operacij bezlich raziv napriklad pri formuvanni kon yunkcij abo diz yunkcij naboru BDR mozhut prizvesti do eksponencialno velikogo BDR v girshomu vipadku Ce vidbuvayetsya cherez te sho rezultatom bud yakih poperednih operacij nad dvoma BDR v zagalnomu vipadku mozhe buti BDR z rozmirom proporcijnim dobutku poperednih rozmiriv tomu dlya dekilkoh BDR rozmir mozhe zbilshuvatisya eksponencialno Div takozh red Zadacha zdijsnennosti bulovih formul Buleva AlgebraPrimitki red Graph Based Algorithms for Boolean Function Manipulation Randal E Bryant 1986 C Y Lee Sheldon B Akers Raymond T Boute The Binary Decision Machine as a programmable controller Randal E Bryant R E Bryant Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams Arhivovano 23 veresnya 2015 u Wayback Machine ACM Computing Surveys Vol 24 No 3 September 1992 pp 293 318 Karl S Brace Richard L Rudell and Randal E Bryant 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 Rekomendovana literatura red D E Knuth The Art of Computer Programming Volume 4 Fascicle 1 Bitwise tricks amp techniques Binary Decision Diagrams Addison Wesley Professional March 27 2009 viii 260pp ISBN 0 321 58050 8 Draft of Fascicle 1b Arhivovano 12 bereznya 2016 u 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 Arhivovano 24 veresnya 2015 u Wayback Machine Springer Verlag Berlin Heidelberg New York 1998 Complete textbook available for download Rudiger Ebendt Gorschwin 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 Posilannya red ABCD Arhivovano 24 zhovtnya 2020 u Wayback Machine The ABCD package by Armin Biere Johannes Kepler Universitat Linz CMU BDD Arhivovano 26 veresnya 2011 u Wayback Machine BDD package Carnegie Mellon University Pittsburgh CUDD BDD package University of Colorado Boulder Installing CUDD in Windows Visual Studio environments Biddy Arhivovano 6 zhovtnya 2015 u Wayback Machine multi platform academic BDD package University of Maribor Slovenia JavaBDD Arhivovano 22 kvitnya 2020 u Wayback Machine 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 Arhivovano 12 lipnya 2012 u Wayback Machine includes a BDD boolean logic simplifier supporting up to 32 inputs 32 outputs independently DDD Arhivovano 9 lipnya 2017 u Wayback Machine 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 Otrimano z https uk wikipedia org w index php title Binarna diagrama rishen amp oldid 40426497