ROBDD является компактным представлением ДНФ (в частности, ортогональных ДНФ). Операции над ROBDD характеризуются полиномиальной сложностью, в то время как операции над ДНФ характеризуются экспоненциальной сложностью [6]. ROBDD является приведённой упорядоченной бинарной разрешающей диаграммой. В настоящее время этот граф позволяет решать множество задач. ROBDD широко используются в системах автоматизированного проектирования (САПР) для синтеза логических схем [4] и в формальной верификации[5]. Поэтому задача более компактного представления является актуальной задачей.
В частности, в данной работе рассматривается задача упрощения графа, являющаяся частью задачи построения установочной последовательности [1]. Где для поиска установочной последовательности используются ROBDD графы, а при построении последовательности используются операции над ROBDD. Перемножение предлагается применять к полным ROBDD графам, а суммирование проводить с использованием фрагментов ROBDD графов, причем эти фрагменты получаются путем применения процедуры упрощения к ROBDD графам, полученным в результате перемножения.
Задача упрощения выполняется с целью уменьшения вычислительных затрат при выполнении операций над ROBDD графами. В данной работе упрощение графа предлагается выполнять с помощью дерева декомпозиции [1]. Дерево декомпозиции строится относительно множества троичных векторов, представляющих путь в ROBDD графе из рассматриваемой вершины в терминальную вершину 1. Дерево строится с помощью процедуры разбиения относительно выбранной переменной, до тех пор, пока в подмножествах не останется неоднородных переменных. В результате такого разбиения терминальным вершинам будут соответствовать всевозможные подмножества троичных векторов однородные по всем переменным или другим словами совместимые подмножества.
Любое совместимое подмножество можно представить в виде троичного вектора, полученного в результате пересечения всех элементов этого множества. Такая процедура позволяет сократить исходное множество троичных векторов. С целью получения оптимального решения нужно рассматривать максимально совместимые подмножества. Такой подход предлагается применить к сокращению ROBDD графа, где начальное множество троичных векторов, представляет собой все пути, рассматриваемого графа, идущие из корневой вершины в терминальную вершину со значением 1. В данной работе представлен алгоритм построения дерева декомпозиции точным методом, а также с применением эвристического подхода, позволяющий сократить вычислительные затраты при построении решения.
Была решена задача упрощения ROBDD графа, в основе которого лежит операция совмещения путей графа. Эти пути были сформированы в результате применения дерева декомпозиции, благодаря которому мы получили совмещенные подмножества, а затем, сперва применив точный метод, а затем эвристические подходы для разложения дерева декомпозиции было получено минимизированное решение. Были проведены экспериментальные результаты, по итогам которых можно заметить, что точный метод позволяет получить максимально совместимые подмножества, но на него уходит очень много времени. Эвристический подход ухудшает результат, но времени на него уходит гораздо меньше.
