Диаграмма двоичных решений

редактировать

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

Содержание

1 Определение
- 1.1 Пример
2 История
3 Приложения
4 Порядок переменных
5 Логические операции на BDD
6 См. Также
7 Ссылки
8 Дополнительная литература
9 Внешние ссылки

Определение

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

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

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

Путь от корневого узла до 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 показан на правом рисунке.

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

f (x 1, x 2, x 3) = x ¯ 1 x ¯ 2 x ¯ 3 + x 1 x 2 + x 2 х 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}}

f (x_ {1}, x_ {2}, x_ {3}) = {\ bar {x}} _ {1} {\ bar {x}} _ {2} {\ bar {x}} _ {3} + x_ {1} x_ {2} + x_ {2} x_ {3}

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

История

Основная идея, из которой структура была создана - это расширение Шеннона. Функция переключения разбивается на две подфункции (кофакторы) путем присвоения одной переменной (см. Нормальную форму if-then-else). Если такая подфункция рассматривается как поддерево, она может быть представлена как. Диаграммы двоичных решений (BDD) были введены Ли, а затем изучены и представлены Акерсом и Баутом.

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

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

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

Приложения

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

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

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

Размер BDD определяется как представляемой функцией, так и выбранным порядком переменных. Существуют булевы функции $f (x 1,…, xn) {\ displaystyle f (x_ {1}, \ ldots, x_ {n})}$ $f (x_ {1}, \ ldots, x _ {{n}})$ , для которых в зависимости от порядка переменных мы бы получили граф, количество узлов которого было бы линейным (по n) в лучшем случае и экспоненциальным в худшем случае (например, сумматор с переносом пульсации ). Рассмотрим булеву функцию $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}.}$ $f (x_ {1}, \ ldots, x _ {{2n}}) = x_ {1} x_ {2} + x_ {3} x_ {4} + \ cdots + x _ {{2n-1}} x _ {{2n}}.$ Используя порядок переменных $x 1 < x 3 < ⋯ < x 2 n − 1 < x 2 < x 4 < ⋯ < x 2 n {\displaystyle x_{1}$ $x_ {1} <x_ {3} <\ cdots <x _ {{2n-1}} <x_ {2} <x_ {4} <\ cdots <x_{{2n}}$ , BDD необходимо 2 узла для представления функции. Используя порядок $x 1 < x 2 < x 3 < x 4 < ⋯ < x 2 n − 1 < x 2 n {\displaystyle x_{1}$ $x_ {1} <x_ {2} <x_ {3} <x_ {4} <\ cdots <x _ {{2n-1} } <x _ {{2n}}$ , BDD состоит из 2n + 2 узлов.

BDD для функции ƒ (x 1,..., x 8) = x 1x2+ x 3x4+ x 5x6+ x 7x8использование неправильного порядка переменных

Хорошее упорядочение переменных

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

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

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

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

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

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

См. Также

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

Ссылки

Дополнительная литература

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

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

Викискладе есть медиафайлы, связанные с диаграммами двоичных решений.

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