Диаграмма двоичного решения - Binary decision diagram

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

Подобные структуры данных включают нормальную форму отрицания (NNF), многочлены Жегалкина и пропозиционально ориентированные ациклические графы (PDAG).

Определение

Логическая функция может быть представлена ​​в виде ориентированного ациклического графа с корнем , который состоит из нескольких (решающих) узлов и двух конечных узлов. Два конечных узла помечены 0 (ЛОЖЬ) и 1 (ИСТИНА). Каждый узел (решение) помечен логической переменной и имеет два дочерних узла, называемых младшим и старшим. Переход от узла к нижнему (или высокому) дочернему элементу представляет присвоение переменной значения FALSE (или TRUE, соответственно) . Такой BDD называется «упорядоченным», если разные переменные появляются в одном порядке на всех путях от корня. BDD называется сокращенным, если к его графу были применены следующие два правила:

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

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

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

Пример

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

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

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

Еще одно обозначение для записи этой логической функции - .

Дополненные края

Диаграмма диаграммы бинарных решений, представленная с использованием дополненных ребер.
Диаграмма диаграммы бинарных решений, представленная с использованием дополненных ребер.

ROBDD можно представить еще более компактно, используя дополненные края. Дополненные края формируются путем аннотирования нижних краев как дополненных или нет. Если ребро дополняется, то это относится к отрицанию логической функции, которая соответствует узлу, на который указывает ребро (логическая функция, представленная BDD с корнем этого узла). Высокие края не дополняются, чтобы гарантировать, что результирующее представление BDD является канонической формой. В этом представлении BDD имеют единственный листовой узел по причинам, объясненным ниже.

Два преимущества использования дополненных краев при представлении BDD:

  • вычисление отрицания BDD занимает постоянное время
  • использование пространства (т.е. требуемая память) уменьшается

Ссылка на BDD в этом представлении представляет собой (возможно, дополненное) «ребро», которое указывает на корень BDD. Это контрастирует со ссылкой на BDD в представлении без использования дополненных ребер, которое является корневым узлом BDD. Причина, по которой ссылка в этом представлении должна быть ребром, заключается в том, что для каждой логической функции функция и ее отрицание представлены ребром к корню BDD и дополненным ребром к корню того же BDD. Вот почему отрицание занимает постоянное время. Это также объясняет, почему достаточно одного листового узла: FALSE представлено дополненным ребром, которое указывает на листовой узел, а TRUE представлено обычным ребром (т. Е. Не дополненным), которое указывает на листовой узел.

Например, предположим, что логическая функция представлена ​​с помощью BDD, представленного с помощью дополненных ребер. Чтобы найти значение логической функции для данного присвоения (логических) значений переменным, мы начинаем с опорного края, который указывает на корень BDD, и следуем по пути, который определяется заданными значениями переменных (после нижний край, если переменная, маркирующая узел, равна ЛОЖЬ, и следующее за верхним краем, если переменная, маркирующая узел, равна ИСТИНА), пока мы не достигнем конечного узла. Следуя по этому пути, мы подсчитываем, сколько дополнительных ребер мы прошли. Если при достижении листового узла мы пересекли нечетное количество дополняемых ребер, то значение логической функции для данного присвоения переменной равно ЛОЖЬ, в противном случае (если мы пересекли четное число дополняемых ребер), тогда значение логическая функция для данного присвоения переменной - ИСТИНА.

Пример диаграммы BDD в этом представлении показан справа и представляет то же логическое выражение, что и на диаграммах выше, т . Е .. Нижние края обозначены пунктиром, высокие - сплошными, а дополненные края обозначены меткой «-1». Узел, метка которого начинается с символа @, представляет ссылку на BDD, т. Е. Опорная кромка - это кромка, которая начинается с этого узла.

История

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

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

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

Приложения

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

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

Переменный порядок

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

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

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

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

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

Логические операции с BDD

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

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

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

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

Смотрите также

использованная литература

дальнейшее чтение

внешние ссылки