Бинарная диаграмма решений

«Разветвление программы» перенаправляется сюда. Чтобы узнать о других значениях, см. NC (сложность) § Теорема Баррингтона .

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

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

Определение

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

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

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

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

Пример

На левом рисунке ниже показано двоичное решений дерево (правила редукции не применяются) и таблица истинности , каждая из которых представляет функцию $f(x_{1},x_{2},x_{3})$. В дереве слева значение функции можно определить для данного назначения переменной, следуя по пути вниз по графику к терминалу. На рисунках ниже пунктирные линии обозначают края младшего дочернего элемента, а сплошные линии представляют края старшего дочернего элемента. Следовательно, чтобы найти $f(0,1,1)$, начните с x ₁ , пройдите вниз по пунктирной линии до x ₂ (поскольку x ₁ присвоено значение 0), затем вниз по двум сплошным линиям (поскольку x ₂ и x ₃ имеют присвоение единице). Это ведет к клемме 1, которая является значением $f(0,1,1)$.

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

Бинарное дерево решений и таблица истинности для функции $f(x_{1},x_{2},x_{3})=(\neg x_{1}\wedge \neg x_{2}\wedge \neg x_{3})\vee (x_{1}\wedge x_{2})\vee (x_{2}\wedge x_{3})$, описанный в обозначениях для булевых операторов .

BDD для функции f

Другое обозначение для записи этой булевой функции: ${\overline {x}}_{1}{\overline {x}}_{2}{\overline {x}}_{3}+x_{1}x_{2}+x_{2}x_{3}$.

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

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

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

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

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

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

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

Пример диаграммы BDD в этом представлении показан справа и представляет то же логическое выражение, что и на диаграммах выше, т.е. $(\neg x_{1}\wedge \neg x_{2}\wedge \neg x_{3})\vee (x_{1}\wedge x_{2})\vee (x_{2}\wedge x_{3})$. Нижние ребра обозначены пунктиром, высокие — сплошными, а дополненные ребра обозначены кружком в начале. Узел с символом @ представляет ссылку на BDD, т. е. опорное ребро — это ребро, которое начинается с этого узла.

История

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

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

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

Приложения

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

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

BDD применяются в эффективных интерпретаторах Datalog .

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

Размер BDD определяется как представляемой функцией, так и выбранным порядком переменных. Существуют булевы функции $f(x_{1},\ldots ,x_{n})$ для которого в зависимости от порядка переменных мы в конечном итоге получим граф, число узлов которого будет в лучшем случае линейным (по n ), а в худшем — экспоненциальным (например, сумматор с пульсирующим переносом ). Рассмотрим булеву функцию $f(x_{1},\ldots ,x_{2n})=x_{1}x_{2}+x_{3}x_{4}+\cdots +x_{2n-1}x_{2n}.$ Использование порядка переменных $x_{1}<x_{3}<\cdots <x_{2n-1}<x_{2}<x_{4}<\cdots <x_{2n}$, БДД нужен $2^{n+1}$ узлы для представления функции. Использование порядка $x_{1}<x_{2}<x_{3}<x_{4}<\cdots <x_{2n-1}<x_{2n}$, BDD состоит из $2n+2$ узлы.

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 раз превышает оптимальный. Однако существуют эффективные эвристики для решения этой проблемы.

Существуют функции, для которых размер графика всегда экспоненциальный, независимо от порядка переменных. Это справедливо, например, для функции умножения. Фактически, функция, вычисляющая средний бит произведения двух $n$-битные числа не имеют OBDD меньше, чем $2^{\lfloor n/2\rfloor }/61-4$ вершины. (Если бы функция умножения имела OBDD полиномиального размера, это показало бы, что факторизация целых чисел находится в P/poly , что, как известно, не соответствует действительности. )

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

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

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

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

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

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

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

См. также

• Булева проблема выполнимости , каноническая NP-полная вычислительная задача
• L/poly — класс сложности , который строго содержит набор задач с BDD полиномиального размера.
• Проверка модели
• Радикс-дерево
• Теорема Баррингтона
• Аппаратное ускорение
• Карта Карно , метод упрощения выражений булевой алгебры
• Диаграмма принятия решений с подавлением нуля
• Алгебраическая диаграмма решений , обобщение BDD от двухэлементных до произвольных конечных множеств.
• Сентенциальная диаграмма принятия решений , обобщение OBDD
• Диаграмма влияния

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

• Убар, Р. (1976). «Генерация тестов для цифровых схем с использованием альтернативных графов». Учеб. Таллиннский технический университет (на русском языке) (409). Таллинн, Эстония: 75–81.
• Кнут, DE (2009). Глава 1: Побитовые трюки и методы; Бинарные диаграммы решений . Искусство компьютерного программирования . Том. 4. Аддисон–Уэсли. ISBN  978-0-321-58050-4 . Черновик главы 1b, заархивированный 12 марта 2016 г. на Wayback Machine, доступен для скачивания.
• Мейнель, К.; Теобальд, Т. (2012) [1998]. Алгоритмы и структуры данных в проектировании СБИС: OBDD – Основы и приложения (PDF) . Спрингер. ISBN  978-3-642-58940-9 . Полный учебник доступен для скачивания.
• Эбендт, Рюдигер; Фей, Гёршвин; Дрекслер, Рольф (2005). Расширенная оптимизация BDD . Спрингер. ISBN  978-0-387-25453-1 .
• Беккер, Бернд; Дрекслер, Рольф (1998). Бинарные диаграммы решений: теория и реализация . Спрингер. ISBN  978-1-4419-5047-5 .

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

• Забавы с двоичными диаграммами решений (BDD) , лекция Дональда Кнута
• Список программных библиотек BDD для нескольких языков программирования.