Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

В информатике , A двоичного решения диаграмма ( BDD ) или разветвленность программа представляет собой структуру данных , которая используется для представления булевой функции . На более абстрактном уровне BDD можно рассматривать как сжатое представление наборов или отношений . В отличие от других сжатых представлений, операции выполняются непосредственно над сжатым представлением, то есть без декомпрессии. Другие структуры данных, используемые для представления булевых функций, включают нормальную форму отрицания (NNF), полиномы Жегалкина ипропозиционально ориентированные ациклические графы (PDAG).

Определение [ править ]

Логическая функция может быть представлена ​​в виде ориентированного ациклического графа с корнем , который состоит из нескольких узлов решений и конечных узлов. Есть два типа терминальных узлов, называемых 0-терминальными и 1-терминальными. Каждый узел решения помечен логической переменной и имеет два дочерних узла, которые называются младшим и старшим. Ребро от узла к нижнему (или высокому) дочернему элементу представляет присвоение 0 (соответственно 1). Такой BDD называется «упорядоченным», если разные переменные появляются в одном порядке на всех путях от корня. BDD называется сокращенным, если к его графу были применены следующие два правила:

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

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

Путь от корневого узла к 1-терминалу представляет собой (возможно, частичное) присвоение переменной, для которой представленная логическая функция истинна. Когда путь спускается к младшему (или высокому) дочернему элементу от узла, переменной этого узла присваивается значение 0 (соответственно 1).

Пример [ править ]

На левом рисунке ниже показано двоичное дерево решений (правила сокращения не применяются) и таблицу истинности , каждая из которых представляет функцию f (x1, x2, x3). В дереве слева значение функции можно определить для заданного присвоения переменной, пройдя путь вниз по графику к терминалу. На рисунках ниже пунктирные линии представляют края младшего дочернего элемента, а сплошные линии - края высокого дочернего элемента. Следовательно, чтобы найти (x1 = 0, x2 = 1, x3 = 1), начните с x1, проведите вниз по пунктирной линии до x2 (так как x1 имеет присвоение 0), затем вниз по двум сплошным линиям (поскольку x2 и x3 каждая есть задание к одному). Это приводит к выводу 1, который является значением f (x1 = 0, x2 = 1, x3 = 1).

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

Дерево двоичных решений и таблица истинности для функции
BDD для функции f

История [ править ]

Основная идея, на основе которой была создана структура данных, - это расширение Шеннона . Функция переключения разделяется на две подфункции (кофакторы) путем присвоения одной переменной (см. Нормальную форму if-then-else ). Если такая подфункция рассматривается как поддерево, она может быть представлена двоичным деревом решений . Диаграммы двоичных решений (BDD) были введены Ли [2], а их дальнейшее изучение и распространение получили Акерс [3] и Буте. [4] Независимо от этих авторов, BDD под названием «каноническая скобочная форма» был реализован Мамруковым в САПР для анализа схем, не зависящих от скорости. [5]Полный потенциал эффективных алгоритмов, основанных на структуре данных, исследовал Рэндал Брайант из Университета Карнеги-Меллона : его ключевые расширения заключались в использовании фиксированного порядка переменных (для канонического представления) и общих подграфов (для сжатия). Применение этих двух концепций приводит к эффективной структуре данных и алгоритмам для представления множеств и отношений. [6] [7] Распространяя совместное использование на несколько BDD, т. Е. Один подграф используется несколькими BDD, определяется структура данных Shared Reduced Ordered Binary Decision Diagram . [8] В настоящее время понятие BDD обычно используется для обозначения этой конкретной структуры данных.

В своем видео - лекции Fun With Binary Decision Diagrams (БДДС) , [9] Дональд Кнут называет БДДС «один из только действительно фундаментальных структур данных , которые вышли в последние двадцать пять лет» и отмечает , что 1986 статьи Брайанта была какое - то время одна из самых цитируемых статей в области компьютерных наук.

Аднан Дарвиче и его сотрудники показали, что BDD - это одна из нескольких нормальных форм для булевых функций, каждая из которых вызвана различным сочетанием требований. Другая важная нормальная форма, определенная Дарвишем, - это нормальная форма разлагаемого отрицания или DNNF.

Приложения [ править ]

BDD широко используются в программном обеспечении САПР для синтеза схем ( логический синтез ) и формальной проверки . Существует несколько менее известных приложений BDD, включая анализ дерева отказов, байесовское рассуждение, конфигурацию продукта и поиск частной информации . [10] [11] [ необходима ссылка ]

Каждый произвольный BDD (даже если он не сокращен или не упорядочен) может быть напрямую реализован на аппаратном уровне путем замены каждого узла мультиплексором 2 к 1 ; каждый мультиплексор может быть напрямую реализован с помощью 4-LUT в FPGA . Это не так просто , чтобы преобразовать из произвольной сети логических вентилей к BDD [ править ] ( в отличие от и-инвертора графике ).

Порядок переменных [ править ]

Размер BDD определяется как представляемой функцией, так и выбранным порядком переменных. Существуют булевы функции, для которых в зависимости от порядка переменных мы в конечном итоге получим граф, количество узлов которого будет линейным (по  n ) в лучшем случае и экспоненциальным в худшем случае (например, сумматор с волновым переносом ). Рассмотрим логическую функцию. Используя порядок переменных , BDD необходимо 2 n +1 узлов для представления функции. Согласно порядку , BDD состоит из 2 n  + 2 узлов.

BDD для функции ƒ ( x 1 , ..., x 8 ) = x 1 x 2 + x 3 x 4 + x 5 x 6 + x 7 x 8 с использованием неправильного порядка переменных
Хороший порядок переменных

При применении этой структуры данных на практике крайне важно позаботиться об упорядочивании переменных. Проблема поиска наилучшего порядка переменных является NP-сложной . [12] Для любой константы c  > 1 даже NP-сложно вычислить упорядочение переменных, что приведет к OBDD с размером, который не более чем в c раз больше оптимального. [13] Однако существуют эффективные эвристики для решения этой проблемы. [14]

Есть функции, для которых размер графика всегда экспоненциальный - независимо от порядка переменных. Это верно, например, для функции умножения. [1] Фактически, функция, вычисляющая средний бит произведения двухбитовых чисел, не имеет OBDD меньше вершин. [15] (Если бы функция умножения имела OBDD полиномиального размера, она показала бы, что целочисленная факторизация выполняется в P / poly , что, как известно, неверно. [16] )

Для клеточных автоматов с простым поведением минимальный BDD обычно растет линейно на последовательных шагах. Например, для правила 254 это 8t + 2, а для правила 90 - 4t + 2. Для клеточных автоматов с более сложным поведением он обычно растет примерно по экспоненте. Таким образом, для правила 30 это {7, 14, 29, 60, 129}, а для правила 110 - {7, 15, 27, 52, 88}. Размер минимального BDD может зависеть от порядка, в котором указаны переменные; таким образом, например, простое отражение правила 30 для правила 86 дает {6, 11, 20, 36, 63}.

Исследователи предложили усовершенствования структуры данных BDD, уступив место ряду связанных графиков, таких как BMD ( диаграммы двоичных моментов ), ZDD ( диаграмма решений с подавлением нуля ), FDD ( диаграммы свободных двоичных решений ), PDD ( диаграммы решений по четности ). и MTBDD (множественные терминальные BDD).

Логические операции с BDD [ править ]

Многие логические операции с BDD могут быть реализованы с помощью алгоритмов манипулирования графами с полиномиальным временем: [17] : 20

  • соединение
  • дизъюнкция
  • отрицание

Однако повторение этих операций несколько раз, например формирование соединения или разъединения набора BDD, может в худшем случае привести к экспоненциально большому BDD. Это связано с тем, что любая из предшествующих операций для двух BDD может привести к BDD с размером, пропорциональным произведению размеров BDD, и, следовательно, для нескольких BDD размер может быть экспоненциальным. Кроме того, поскольку построение BDD булевой функции решает NP-полную проблему булевой выполнимости и проблему co-NP-полной тавтологии , построение BDD может занять экспоненциальное время в размере булевой формулы, даже если результирующий BDD невелик.

Вычисление экзистенциальной абстракции над несколькими переменными сокращенных BDD является NP-полным. [18]

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

См. Также [ править ]

  • Проблема булевой выполнимости , каноническая NP-полная вычислительная задача
  • L / poly , класс сложности, который строго содержит набор задач с BDD полиномиального размера [ необходима ссылка ]
  • Проверка модели
  • Основное дерево
  • Теорема Баррингтона
  • Аппаратное ускорение
  • Карта Карно , метод упрощения выражений булевой алгебры

Ссылки [ править ]

  1. ^ a b Графические алгоритмы для манипуляции логическими функциями, Рэндал Э. Брайант, 1986
  2. ^ CY Ли. "Представление коммутационных цепей программами двоичного решения". Технический журнал Bell System, 38: 985–999, 1959.
  3. ^ Шелдон Б. Акерс-младший . Диаграммы двоичных решений, транзакции IEEE на компьютерах, C-27 (6): 509–516, июнь 1978.
  4. ^ Раймонд Т. Бут, "Машина двоичных решений как программируемый контроллер". Информационный бюллетень EUROMICRO , Vol. 1 (2): 16–22, январь 1976 г.
  5. ^ Ю. Мамруков В. Анализ апериодических цепей и асинхронных процессов. Кандидат наук. диссертация. Ленинградский электротехнический институт, 1984, 219 с.
  6. ^ Рэндал Э. Брайант. " Графические алгоритмы для манипуляции логическими функциями ". IEEE Transactions on Computers, C-35 (8): 677–691, 1986.
  7. ^ Рэндал Э. Брайант, " Символьные логические манипуляции с упорядоченными двоичными диаграммами решений" , ACM Computing Surveys, Vol. 24, № 3 (сентябрь 1992 г.), стр. 293–318.
  8. ^ Карл С. Брейс, Ричард Л. Руделл и Рэндал Э. Брайант. « Эффективное внедрение пакета BDD» . В материалах 27-й конференции по автоматизации проектирования ACM / IEEE (DAC 1990), страницы 40–45. Издательство IEEE Computer Society Press, 1990.
  9. ^ "Стэнфордский центр профессионального развития" . scpd.stanford.edu . Архивировано из оригинала на 2014-06-04 . Проверено 23 апреля 2018 .
  10. ^ РМ Дженсен. «CLab: библиотека C ++ для быстрой интерактивной конфигурации продукта без возврата» . Труды Десятой Международной конференции по принципам и практике программирования с ограничениями, 2004 г.
  11. ^ HL Lipmaa. «Первый протокол CPIR с вычислением, зависящим от данных» . ICISC 2009.
  12. ^ Беата Bollig, Инго Вегенер. Улучшение порядка переменных в OBDD полностью завершено , IEEE Transactions on Computers, 45 (9): 993–1002, сентябрь 1996 г.
  13. ^ Детлеф Зилинг. «Неприблизимость минимизации OBDD». Информация и вычисления 172, 103–138. 2002 г.
  14. ↑ Райс, Майкл. «Обзор эвристики упорядочивания статических переменных для эффективного построения BDD / MDD» (PDF) .
  15. ^ Филипп Вельфель. « Границы OBDD-размера целочисленного умножения посредством универсального хеширования ». Журнал компьютерных и системных наук 71, стр. 520-534, 2005.
  16. ^ Ричард Дж. Липтон . «БДД и факторинг» . Утерянное письмо Гёделя и P = NP , 2009.
  17. ^ Андерсен, HR (1999). «Введение в двоичные диаграммы решений» (PDF) . Конспект лекций . ИТ-университет Копенгагена.
  18. ^ Хут, Майкл; Райан, Марк (2004). Логика в информатике: моделирование и рассуждения о системах (2-е изд.). Кембридж [Великобритания]: Издательство Кембриджского университета. С. 380–. ISBN 978-0-52154310-1. OCLC  54960031 .

Дальнейшее чтение [ править ]

  • Р. Убар, "Генерация тестов для цифровых схем с использованием альтернативных графов", в сб. Таллиннский технический университет, 1976, № 409, Таллиннский технический университет, Таллинн, Эстония, стр. 75–81.
  • Д. Кнут, « Искусство компьютерного программирования, том 4, часть 1: побитовые приемы и методы; диаграммы двоичных решений» (Addison – Wesley Professional, 27 марта 2009 г.) viii + 260pp, ISBN 0-321-58050-8 . Черновик Fascicle 1b доступен для скачивания. 
  • Гл. Майнель, Т. Теобальд, " Алгоритмы и структуры данных в СБИС-проектировании: OBDD - основы и приложения" , Springer-Verlag, Берлин, Гейдельберг, Нью-Йорк, 1998. Полный учебник доступен для загрузки.
  • Эбендт, Рюдигер; Фей, Гёршвин; Дрекслер, Рольф (2005). Расширенная оптимизация BDD . Springer. ISBN 978-0-387-25453-1.
  • Беккер, Бернд; Дрекслер, Рольф (1998). Диаграммы двоичных решений: теория и реализация . Springer. ISBN 978-1-4419-5047-5.

Внешние ссылки [ править ]

  • Fun With Binary Decision Diagrams (BDDs) , лекция Дональда Кнута
  • Список программных библиотек BDD для нескольких языков программирования.