Use of binary decision diagrams in theproblems of discrete functions inversing .pdf Двоичные диаграммы решений (Binary Decision Diagram, BDD) - это специальный вид направленных помеченных графов, посредством которых можно представлять булевы функции. Образно говоря, BDD (а точнее ROBDD) решают проблему компактного представления булевых функций «в классе графов». Несмотря на то, что первое упоминание BDD (под названием «двоичные решающие программы») встречается в статье [1] (1959 г.), осознание значимости BDD для математической и прикладной кибернетики пришло после фундаментальной работы Р.Е. Брайанта [2] (1986 г.).В настоящей статье анализируется применимость BDD в задачах обращения дискретных функций из класса 3 (см. [3]), известного своими многочисленными приложениями в дискретной математике и математической кибернетике (в частности, в криптографии).1 Работа выполнена при поддержке гранта РФФИ № 07-01-00400-а и при поддержке гранта Президента РФ НШ-1676.2008.1.В первом разделе приводятся основные понятия и определения. Во втором разделе описан BDD-подход к решению систем логических уравнений (особый акцент сделан на системах, кодирующих задачи обращения функций из класса 3). В третьем разделе приведено краткое описание «гибридного» подхода к решению логических уравнений - в рамках данного подхода BDD используются в качестве модифицируемых структур данных, сохраняющих информацию о процессе DPLL-вывода. В четвертом разделе анализируются особенности архитектуры «типового» BDD-решателя систем логических уравнений.1. Основные определения и понятияЛогическими уравнениями называются выражения вида L(x),..., Xn) = 0, L(x1,..., xn) = 1, где через L (x1,...,xn) обозначается формула (исчисления высказываний), задающая некоторую булеву функцию над множеством булевых переменных X = {x1,...,xn}. Тот факт, что при подстановке x1 =а1,...,xn =an, ai е{0,1),i е{1,...,n}, формула L(x1,...,xn) принимает значение ße{0,1} обозначается через L(x1,...,xn)\( a )=ß (или более кратко через L \( a )=ß). Если существует такой набор (а1,..., an), ai е{0,1}, i е{1,..., n}, значений переменных x1,..., xn, что L \(а1 а )=ß , то данный набор называется решением логического уравнения L (x1,..., xn) = ß. Системой логических уравнений называется выражение вида' L1 (X1,..., xn ) = ß1,, (1).Lm (x1,..., xn ) = ßmпри фиксированных значениях булевых констант ßj, j е {1,...,m}. Решением системы (1) называется набор значений переменных (x1,...,xn), являющийся решением всех уравнений системы. Если такого набора не существует, то говорят, что система (1) несовместна. Очевидно, что произвольная система логических уравнений вида (1) может быть эффективно преобразована к виду'L 1 (x1,.-xn ) = 1>■, (2).L m (xl,..., xn)=1.Система (2) эквивалентна одному логическому уравнению видаL1 (x1,.-xn )■... ■L m (xl,..., xn )=1.Введем в рассмотрение булеву функцию L : {0,1}n -> {0,1} , определяемую следующим образом:L (a) = (L 1 (x1,.-xn )^... ^L'm (x1,..., xn ))\a, ae{0,1}n .Данную функцию назовем характеристической функцией системы (1).Двоичная диаграмма решений (BDD) (см., например [4]) определяется как направленный ациклический граф, в котором выделена одна вершина с входной степенью 0, называемая корнем, и две вершины с выходной степенью 0, называемые терминальными. Терминальные вершины помечены константами 0 и 1. Все остальные вершины помечаются переменными из множества X = {x1,...,xn}. Излюбой вершины, за исключением терминальных, выходят в точности 2 дуги. Одну дугу обычно рисуют пунктирной, а другую - сплошной линией. Дуга, обозначенная пунктиром, называется low-ребром, дуга, обозначенная сплошной линией, -high-ребром. Простейшие примеры BDD получаются объединением одноименных листьев в двоичных деревьях решений.Деревья решений (см, например [4]) суть помеченные деревья, используемые в различных разделах дискретной математики. Обозначим через {0,1}n, n е N, множество всех двоичных слов (последовательностей) длины n. Функции вида fn : {0,1}n - {0,1} называются булевыми функциями над множеством булевых переменных X = {x1,..., xn}. Пусть fn - произвольная всюду определенная булевафункция. Сопоставим ей двоичное дерево решений, построенное в соответствии с перечисленными ниже правилами. Вершины (узлы) дерева соответствуют булевым переменным. Пунктирное ребро, исходящее из узла, помеченного переменной xi,i е{1,...,n}, означает, что данная переменная принимает значение 0,сплошное ребро соответствует тому, что xi принимает значение 1. Листья деревапомечены значениями рассматриваемой функции при соответствующих наборах значений булевых переменных. Произвольный путь из корня в лист, помеченный ае {0,1} , определяет набор или семейство наборов значений переменных, на которых рассматриваемая функция принимает значение а . Пусть fn : {0,1}n - {0,1} - произвольная всюду определенная булева функция над множеством булевых переменных X = {x1,..., xn} и T (fn) - ее дерево решений. Если объединить в одну вершину все листья дерева T (fn), помеченные нулем, и то же самое проделать с листьями, помеченными единицей, получится BDD. Если произвольный путь п в BDD из корня в терминальную вершину не содержит вершин, помеченных одинаковыми переменными, и его прохождение подчинено общему для всех путей порядку (например, x1 -< x2 -

Скачать электронную версию публикации