Вычисляющая программа — последовательная программная интерпретация схемы вычисления: входные значения помещаются в память, затем выполняются команды вычисления функций над уже полученными значениями и выдаются требуемые результаты. Для такой программы важны не только число команд, но и число промежуточных результатов, которые одновременно должны
BDD (Binary Decision Diagram) — ориентированный ациклический граф принятия решений для булевой функции. Во внутренней вершине проверяется переменная, две исходящие дуги соответствуют значениям 0 и 1, а путь заканчивается в терминале 0 или 1. В отличие от прямой вычисляющей программы, BDD выбирает дальнейшую ветвь по
Что важно запомнить
- Вычисляющая программа задаёт фиксированную последовательность входных, вычислительных и выходных
- Её ширина характеризует максимальное число промежуточных значений, которые одновременно должны оставаться доступными.
- BDD — корневой DAG с вершинами проверки переменных и двумя исходящими
- На конкретном входе BDD вычисляет функцию прохождением одного пути от корня к терминалу.
- Совпадающие остаточные подфункции могут использовать одну общую вершину, поэтому BDD в общем случае является графом, а не деревом.
Вычисляющая программа как последовательная модель
Схему из функциональных элементов можно упорядочить так, чтобы каждый элемент вычислялся только после своих аргументов. Это даёт вычисляющую программу: сначала выполняются команды ввода, затем команды вида «вычислить значение функции от уже доступных результатов», после чего нужные значения выдаются как
Число команд связано с объёмом работы. Отдельный ресурс — рабочая память. Промежуточное значение нужно хранить от момента его вычисления до последнего использования. Ширина программы характеризует наибольшее число таких одновременно «живых» значений и потому моделирует необходимое число ячеек рабочей
Двоичная решающая диаграмма
В BDD внутренние вершины помечены переменными. Из каждой внутренней вершины выходят две дуги: по одной переходят при значении переменной 0, по другой — при значении 1. Терминальные вершины задают значение функции. Для фиксированного входного набора вычисление состоит в прохождении пути от корня до
Стандартное определение BDD допускает объединение одинаковых продолжений вычисления: несколько дуг могут вести в одну и ту же вершину. Благодаря этому повторяющаяся остаточная функция представляется один раз. Если дополнительно вдоль всех путей переменные проверяются в одном фиксированном порядке, получают важный подкласс OBDD.
Различие моделей
Вычисляющая программа без условных переходов выполняет заданную последовательность операций независимо от текущих значений входов. BDD, напротив, является ветвящейся программой: после проверки переменной выполняется только выбранное продолжение. Поэтому размер графа описывает объём представления, а длина конкретного пути — объём работы для данного входа.
Пример простыми словами
Для функции «если \(x_1=0\), вернуть \(x_2\), иначе вернуть \(x_3\)» BDD сначала проверяет \(x_1\). По 0-дуге он переходит к проверке \(x_2\), по 1-дуге — к \(x_3\). Остальная часть графа на данном входе не выполняется.
Частые ошибки
- Считать BDD обычным деревом решений. Общие остаточные подфункции могут быть объединены, поэтому структура является DAG.
- Путать размер BDD и длину вычисления на конкретном входе. Вычисление идёт только по одному пути.
- Отождествлять ширину вычисляющей программы с общим числом команд. Ширина отражает одновременно хранимые промежуточные результаты.
