Введение
Структура данных для булевых функций
В информатике бинарная диаграмма решений (BDD) или программа ветвления — это структура данных, используемая для представления булевой функции. На более абстрактном уровне BDD можно рассматривать как сжатое представление множеств или отношений. В отличие от других способов сжатия данных, операции выполняются непосредственно над сжатым представлением, то есть без распаковки. К схожим структурам данных относятся отрицательная нормальная форма (NNF), многочлены Жегалкина и направленные ациклические графы для логических выражений (PDAG).
Определение
Булева функция может быть представлена как корневой, направленный, ациклический граф, состоящий из нескольких (решающих) узлов и двух терминальных узлов. Два терминальных узла обозначены 0 (ЛОЖЬ) и 1 (ИСТИНА). Каждый (решающий) узел помечен булевой переменной и имеет два дочерних узла, называемых нижним потомком и верхним потомком. Ребро от узла к нижнему (или верхнему) потомку представляет собой присваивание значения ЛОЖЬ (или ИСТИНА, соответственно) переменной. Такой BDD называется «упорядоченным», если различные переменные появляются в одном и том же порядке на всех путях от корня. BDD считается «приведенным», если к его графу применены следующие два правила:
Объединить любые изоморфные подграфы. Удалить любой узел, у которого два потомка изоморфны. В широком употреблении термин BDD почти всегда относится к приведенной упорядоченной бинарной диаграмме принятия решений (ROBDD в литературе, используется, когда необходимо подчеркнуть аспекты упорядочивания и приведения). Преимущество ROBDD заключается в том, что он каноничен (единственен) для конкретной функции и порядка переменных. Полный потенциал эффективных алгоритмов, основанных на этой структуре данных, был исследован Рэндалом Брайантом в Университете Карнеги — Меллона: его ключевыми дополнениями было использование фиксированного порядка переменных (для канонического представления) и общих подграфов (для сжатия). Применение этих двух концепций приводит к эффективной структуре данных и алгоритмам для представления множеств и отношений.
Merge any isomorphic subgraphs. Eliminate any node whose two children are isomorphic. In popular usage, the term BDD almost always refers to Reduced Ordered Binary Decision Diagram (ROBDD in the literature, used when the ordering and reduction aspects need to be emphasized). The advantage of an ROBDD is that it is canonical (unique) for a particular function and variable order. The full potential for efficient algorithms based on the data structure was investigated by Randal Bryant at Carnegie Mellon University: his key extensions were to use a fixed variable ordering (for canonical representation) and shared sub graphs (for compression). Applying these two concepts results in an efficient data structure and algorithms for the representation of sets and relations.
Переменная последовательность
Размер BDD определяется как представляемой функцией, так и выбранным порядком переменных. Существуют булевы функции, для которых, в зависимости от порядка переменных, мы можем получить граф, число узлов которого будет линейным (относительно n) в лучшем случае и экспоненциальным в худшем (например, сумматор с переносом через разряд). Рассмотрим булеву функцию. При использовании порядка переменных, BDD требует узлов для представления функции. При использовании порядка, BDD состоит из узлов. При практическом применении этой структуры данных крайне важно уделять внимание порядку переменных. Задача поиска оптимального порядка переменных является NP-трудной.