Просмотр кода страницы Бинарный граф решений

Ключевые слова и синонимы: '''БДР'''; '''бинарная диаграмма решений'''

== Постановка задачи ==
'''Булевы функции'''

Понятие ''булевой функции'' – функции с областью определения {0,1}<math>^n</math> и областью значений {0,1} – является одним из базовых понятий для любых вычислений. Булевы функции используются в основополагающих работах по вычислительной сложности [7, 9], а также при проектировании и анализе логических схем [4, 13]. Булева функция может быть представлена в виде ''таблицы истинности'' – перечисления значений, принимаемых функцией на каждом элементе {0,1}<math>^n</math>. Поскольку для представления в виде таблицы истинности требуется экспоненциальный относительно n объем памяти, для большинства приложений оно оказывается непрактичным. Следовательно, существует потребность в структурах данных и соответствующих алгоритмах для эффективного представления и обработки булевых функций.

'''Булевы схемы'''

Булевы функции могут быть представлены различными способами. Одним из естественных представлений является ''схема булевых комбинаций'', или просто ''булева схема'' [6, глава 34]. Схема состоит из булевых комбинационных элементов, соединенных ''проводами''. Булевыми комбинационными элементами являются ''вентили'' и ''первичные входы''. Существуют три типа вентилей: NOT, AND и OR. Вентильная функция NOT работает следующим образом: она принимает одно булево ''значение-вход'' и вычисляет одно булево ''значение-выход'', которое принимает значение 0 в случае, если вход равен 1, и 1 – если вход равен 0. Вентиль AND принимает два булевых значения-входа и вычисляет одно значение-выход, равное 1, если оба входа имеют значение 1, и 0 в противном случае. Вентиль OR похож на AND, за тем исключением, что выходное значение равно 1 в случае, если одно или оба входных значения равны 1, и 0 в противном случае.

Схемы должны быть бесконтурными; отсутствие контуров обеспечивает возможность однозначным образом протягивать булево присваивание первичным входам по вентилям в топологическом порядке. Из этого следует, что схема на n упорядоченных первичных входах с выделенным вентилем, называемым ''первичным выходом'', соответствует булевой функции на {0,1}<math>^n</math>. Каждая булева функция может быть представлена схемой – например, путем построения схемы, воспроизводящей таблицу истинности.

Представление в виде схемы имеет слишком общий вид: любая проблема разрешимости, вычислимая на [[Машина Тьюринга|машине Тьюринга]] за полиномиальное время, может быть вычислена при помощи схем полиномиальной относительно размера экземпляра величины, причем схемы могут быть эффективно построены из программы машины Тьюринга [15]. Однако главные задачи анализа на схемах, называемые проблемой выполнимости и проблемой эквивалентности, являются [[NP-Полная задача|NP-полными]] [7].

'''Булевы формулы'''

''Булева формула'' определяется рекурсивным образом: ''булева переменная'' <math>x_i</math> является булевой формулой; если <math>\varphi \,</math> и <math>\psi \, </math> являются булевыми формулами, то ими являются также (<math>\lnot \varphi</math>), (<math>\varphi \land \psi </math>), (<math>\varphi \lor \psi </math>), (<math>\varphi \rightarrow \psi </math>) и (<math>\varphi \leftrightarrow \psi </math>). Операторы <math>\lnot</math>, <math>\land</math>, <math>\lor</math>, <math>\rightarrow</math>, <math>\leftrightarrow</math> называются ''логическими операциями''; ради удобства записи скобки часто опускаются. Булевы формулы могут использоваться для представления произвольных булевых функций; однако проблемы выполнимости и эквивалентности формул также являются NP-полными. Булевы формулы являются менее краткими и сжатыми, чем булевы схемы: к примеру, функция четности имеет схемы линейного размера, тогда как представления в виде формул являются сверхполиномиальными. Точнее говоря, XOR<math>_n</math>: {0, 1}<math>^n</math> <math>\mapsto</math> {0, 1} определена следующим образом: она принимает значение 1 в точности на тех элементах {0, 1}<math>^n</math>, которые содержат нечетное число единиц. Определим ''размер'' формулы, равный количеству встречающихся в ней логических операций. Тогда для любой последовательности формул <math>\theta _1 \, </math>, <math>\theta _2 \, </math>, ... , такой, что <math>\theta _k \, </math> представляет XOR<math>_k</math>, размер <math>\theta _k \, </math> равен <math>\Omega(k^c) \, </math> для всех  <math>c \in Z^+ \, </math> [14 , главы 11 и 12].

''Дизъюнкция'' представляет собой булеву формулу, содержащую только логические операции <math>\land</math> и <math>\lnot</math>, причем  применяется только к переменным; к примеру, x1 <math>\land</math> <math>\lnot</math>x3 <math>\land</math> <math>\lnot</math>x5 является дизъюнкцией. Булева формула находится в ''дизъюнктивной нормальной форме'' (''ДНФ''), если она имеет вид <math>D_0 \lor D_1 \lor ... \lor D_{k-1}</math>, где каждый член <math>D_i</math> является дизъюнкцией. ДНФ-формулы могут представлять произвольные булевы функции, например, путем определения каждого входа, на котором формула принимает значение 1, как дизъюнкции. ДНФ-формулы применяются в проектировании логических схем, поскольку могут быть непосредственно переведены в ПЛМ [4]. Однако если проблема выполнимости ДНФ-формул решается тривиально, то проблема эквивалентности является [[NP-Полная задача|NP-полной]]. Кроме того, если <math>\varphi \, </math> и <math>\psi \,</math>  являются ДНФ-формулами, то <math>\lnot \varphi </math> и <math>\varphi \land \psi </math> таковыми не являются, а перевод их в ДНФ, представляющие ту же функцию, может привести к экспоненциальному росту размера формулы.

'''Деревья Шеннона'''

Пусть f – булева функция на области определения {0,1}<math>^n</math>. Ассоциируем n размерностей с переменными <math>x_0, ..., x_{n-1}</math>. Тогда ''положительным сомножителем'' f относительно <math>x_i</math>, обозначаемым <math>f_{xi}</math>, является функция на области определения {0,1}<math>^n</math>, которая задается следующим образом

<math>f_{xi}( \alpha_0, ... , \alpha_{i-1}, \alpha_i, \alpha_{i+1}, ..., \alpha_{n-1}) = f( \alpha_0, ... ,\alpha_{i-1}, 1, \alpha_{i+1}, ..., \alpha_{n-1}) \, </math>.

''Отрицательный сомножитель'' относительно <math>x_i</math>, обозначаемый <math>f_xi’</math>, определяется точно так же, только на правой стороне вместо 1 стоит 0.

Каждая булева функция может быть подвергнута декомпозиции при помощи теоремы расширения Шеннона:

<math>f(x_1, ... , x_n) = x_i \cdot f_{xi} + x'_i f_{x'i}</math>

Это наблюдение можно использовать для представления f в виде <math>дерево Шеннона|дерева Шеннона</math> – полного бинарного дерева [6, приложение B.5] высоты n, в котором каждый путь в вершину-лист определяет полное присваивание n переменным, над которыми определена функция f; а вершина-лист содержит значение 0 или 1 в зависимости от значения, которое f принимает при присваивании.

Дерево Шеннона нельзя назвать достаточно удобным представлением, поскольку высота дерева, представляющего любую булеву функцию на {0,1}<math>^n</math>, равна n, так что дерево имеет <math>2^n</math> листьев. Дерево Шеннона можно уменьшить при помощи слияния изоморфных поддеревьев и пренебрежения вершинами, имеющими идентичных потомков. На первый взгляд, использование сокращенного дерева Шеннона тоже не особенно практично, поскольку оно включает создание на первом этапе полного бинарного дерева. Более того, пока неясно, как можно на сокращенном дереве Шеннона эффективно производить такие операции, как проверка эквивалентности или вычисление конъюнкции функций, представленных в виде сокращенных деревьев Шеннона.

Брайант [5] пришел к выводу, что накладывание ограничения, согласно которому переменные появляются в фиксированном порядке от корня к листьям, значительно снижает сложность обработки сокращенных деревьев Шеннона. Это представление он назвал ''бинарной диаграммой решений'' (БДР).

== Основные результаты ==
'''Определения'''

Бинарная диаграмма решений (БДР) представляет собой бесконтурный орграф с выдеренной вершиной и не более чем двумя стоками, один из которых имеет метку 0, а другой – метку 1. Вершины, не являющиеся стоками, помечены переменными. Каждая вершина, не являющаяся стоком, имеет две исходящих дуги; одна из них имеет метку 1 и ведет к ''1-потомку'', другая имеет метку 0 и ведет к ''0-потомку''. Переменные должны быть упорядочены; иначе говоря, если переменная-метка <math>x_i</math> появляется раньше метки <math>x_j</math> на некотором пути из вершины к стоку, тогда метка <math>x_j</math> не может встречаться до <math>x_i</math> ни на одном пути из вершины к стоку. Две вершины являются ''изоморфными'', если обе являются стоками с одинаковой меткой либо представляют собой вершины, не являющиеся стоками, с одной и той же переменной-меткой, причем их 0-потомки и 1-потомки изоморфны. Чтобы бесконтурный орграф был допустимой БДР, необходимо, чтобы в нем не было изоморфных вершин и чтобы никакие вершины не имели одинаковых 0-потомков и 1-потомков.

Основной результат теории БДР заключается в следующем: если дано фиксированное упорядочение переменных, то представление является уникальным с точностью до изоморфизма. Иначе говоря, если F и G являются БДР, представляющими f: {0, 1}<math>^n</math> <math>\mapsto</math> {0, 1} с порядком переменных <math>x_1 \prec x_2 \prec ... x_n</math>, то F и G являются изоформными.

Определение изоморфизма напрямую дает нам рекурсивный алгоритм проверки на изоморфизм. Однако он имеет экспоненциальную по отношению к числу узлов сложность; это можно проиллюстрировать, в частности, при помощи проверки изоморфизма БДР для функции четности относительно ее самой. Экспоненциальная сложность связана с постоянно возникающими проверками на изоморфизм между парами вершин; решение может быть найдено в динамическом программировании. Кэширование проверок на изоморфизм снижает сложность этих проверок до O(|F| <math>\cdot </math> |G|), где |B| обозначает количество вершин в БДР B.


'''Операции с БДР'''

Многие логические операции при использовании БДР могут быть реализованы за полиномиальное время: их примерами являются bdd_and, которая вычисляет БДР, представляющую логическое сложение AND функций, представленных двумя БДР, bdd_or и bdd_not определяются аналогичным образом для OR и NOT; bdd_compose принимает БДР, представляющие функции f и g, и переменную v и возвращает БДР для f, в которой v заменена на g.

Пример bdd_and был выбран не случайно: он основан на тождестве <math>f \cdot g = x \cdot (f_x \cdot g_x) + x' \cdot (f_{x'} \cdot g_{x'})</math>. Рекурсия может быть реализована напрямую: основными являются ситуации, когда либо f, либо g равны 0, и когда одно или оба значения равны 1. Рекурсивный процесс выбирает переменную v, являющуюся меткой корня БДР либо для f, либо для g, в зависимости от того, что из них идет раньше по порядку переменных, и, рекурсивно вычисляет БДР для <math>f_v \cdot g_v</math> и <math>f_{v'} \cdot g_{v'}</math>; если они изоморфны, выполняется их слияние. Пусть дана БДР F для f. Если v – переменная, служащая меткой корня F, то БДР для <math>f_{v'} \, </math> и <math>f_v \, </math> представляют собой просто 0-потомка и 1-потомка корня F, соответственно.

Реализация bdd_and вышеописанным способом имеет экспоненциальную сложность из-за постоянного возникновения новых подзадач. Динамическое программирование вновь может стать вариантом решения этой проблемы: кэширование промежуточных результатов bdd_and снижает сложность до O(|F| • |G|).


'''Упорядочение переменных'''

Все симметричные функции на {0,1}<math>^n</math> имеют БДР полиномиального относительно n размера, независимо от порядка переменных. Однако другие полезные функции (например, компараторы, мультиплексоры, сумматоры и вычитатели) могут быть представлены более эффективно, если правильно выбран порядок переменных. Эвристики для выбора упорядочения представлены, например, в [1, 2, 11]. Существуют функции, не имеющие полиномиальных БДР при любом порядке переменных – например, функция, представляющая n-й бит выходного значения мультиплексора, принимающего на вход два n-битных целых числа без знака [5]. Вегенер [17] приводит и другие примеры, доказывающие важность правильного выбора порядка переменных.

== Применение ==
БДР чаще всего применяются в контексте формальной верификации цифрового оборудования [8]. Цифровое оборудование является расширением понятия схемы, описанного выше, путем введения элементов хранения состояния, которые хранят булево значение между обновлениями и обновляются по сигналу синхронизатора.

Вентили, составляющие конструкцию, часто обновляются в силу эксплуатационных требований; эти изменения обычно не предполагают изменения логической функциональности конструкции. Подходы, основанные на использовании БДР, применяются для проверки эквивалентности при проектировании цифрового оборудования [10].

БДР также используются для проверки свойств цифрового оборудования. Типичная формулировка выглядит следующим образом: имеются множество «хороших» состояний и множество «начальных» состояний, определенные при помощи булевых формул над элементами хранения состояния; свойство выполняется в том и только том случае, если не имеется последовательностей входных значений, которые приводят состояние в начальном состоянии в состояние, не входящее в множество хороших состояний. Если имеется конструкция с n регистрами, множество состояний A в конструкции может быть охарактеризовано формулой <math>\varphi_A</math> над n булевыми переменными: <math>\varphi_A</math> расценивает присваивание переменным как истинное в том и только том случае, если соответствующее состояние входит в множество A. Формула <math>\varphi_A</math> представляет булеву функцию; таким образом, для представления множеств состояний могут использоваться БДР. Основная операция вычисления ''образа'' множества состояний системы (то есть множества состояний, которые могут быть достигнуты при применении одного входного значения из состояний множества A) также может быть реализована с использованием БДР [12].

Бинарные диаграммы решений использовались также для ''генерации тестов''. Один из подходов к генерации тестов заключается в задании допустимых входных значений при помощи ограничений, которые, в сущности, являются булевыми формулами над первичным входом и переменными состояния. Юань и коллеги [18] продемонстрировали высокую эффективность БДР в работе с подобными ограничениями.

Синтез логических схем заключается в воплощении аппаратных конструкций, заданных логическими уравнениями, при помощи вентилей. Отображение уравнений на вентили производится тривиальным образом; однако на практике прямое отображение приводит к появлению конструкций, неприемлемых с точки зрения производительности (измеряемой площадью вентильной схемы или временной задержкой). Преобразование логических уравнений для сокращения площади (например, посредством протягивания констант, определения общих подвыражений и т.п.) или задержки (в частности, путем протягивания поздно приходящих сигналов ближе к точкам выхода) обычно производится при помощи БДР.

== Экспериментальные результаты ==
Брайант исследовал возможность проверки двух качественно различных схем для сложения. Ему удалось проверить эквивалентность двух 64-битных сумматоров на VAX 11/780 (компьютере с одним MIP) за 95,8 минут. При этом он использовал выведенное вручную упорядочение.

Современные БДР-пакеты работают на два порядка величины быстрее, чем первая реализация Брайанта. Одним из источников усовершенствования было использование ''строгой канонической формы'', в которой поддерживается глобальная база данных вершин БДР, и ни одна новая вершина не может быть добавлена без проверки, не существует ли уже в базе данных вершины с той же меткой и теми же 0-потомком и 1-потомком [3]. (Для этого требуется, чтобы потомки любой добавляемой вершины также находились в строгой канонической форме). Другими путями к повышению производительности были использование дополнительных указателей (если у указателя установлен наименьший значащий бит, он ссылается на дополнение функции), лучшее управление памятью (сборка мусора на базе счетчиков ссылок, хранение часто используемых вершин в памяти поблизости друг от друга), улучшенные хэш-функции и лучшая организация таблицы вычисленных результатов (в которой отслеживаются подзадачи, уже встреченные ранее) [16].


'''Наборы данных'''

Для синтеза логических схем используется система [http://embedded.eecs.berkeley.edu/pubs/downloads/sis/ SIS] из Калифорнийского университета в Беркли. Она содержит несколько комбинационных и последовательных схем, использовавшихся для эталонного тестирования пакетов БДР.
Система [http://embedded.eecs.berkeley.edu/pubs/downloads/vis VIS] из Калифорнийского университета в Беркли и Колорадского университета в Боулдере применяется для верификации проектов; она использует БДР для проведения проверок. Дистрибутив содержит большой пакет задач верификации, начиная с простых аппаратных схем до сложных мультипроцессорных систем с кэш-памятью.

== Ссылка на код ==
В настоящее время доступно множество пакетов БДР; автор обзора рекомендует пакет [http://vlsi.colorado.edu/~fabio/CUDD/ CUDD]. CUDD реализует все основные функции для работы с БДР и их вариации; он написан на C++ и снабжен полной документацией для пользователя и разработчика.

== См. также ==

* ''[[Символьная проверка на модели]]

== Литература ==
1. Aziz, A., Tasiran,S.,Brayton,R.: BDD Variable Ordering for Interacting Finite State Machines. In: ACM Design Automation Conference, pp. 283-288. (1994)

2. Berman, C.L.: Ordered Binary Decision Diagrams and Circuit Structure. In: IEEE International Conference on Computer Design. (1989)

3. Brace, K., Rudell, R., Bryant, R.: Efficient Implementation of a BDD Package. In: ACM Design Automation Conference. (1990)

4. Brayton, R., Hachtel, G., McMullen, C., Sangiovanni-Vincentelli, A.: Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers (1984)

5. Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transac. Comp. C-35,677-691 (1986)

6. Cormen,T.H., Leiserson, C.E., Rivest, R.H., Stein, C.: Introduction to Algorithms. MIT Press (2001)

7. Garey, M.R., Johnson, D.S.: Computers and Intractability. W.H. Freeman and Co. (1979)

8. Gupta, A.: Formal Hardware Verification Methods: A Survey. Formal Method Syst. Des. 1,151-238 (1993)

9. Karchmer, M.: Communication Complexity: A New Approach to Circuit Depth. MIT Press (1989)

10. Kuehlmann, A., Krohm, F.: Equivalence Checking Using Cuts and Heaps. In: ACM Design Automation Conference (1997)

11. Malik, S., Wang, A.R., Brayton, R.K., Sangiovanni-Vincentelli, A.: Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment. In: IEEE International Conference on Computer-Aided Design, pp. 6-9. (1988)

12. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993)

13. De Micheli, G.: Synthesis and Optimization of Digital Circuits. McGraw Hill (1994)

14. Schoning, U., Pruim, R.: Gems of Theoretical Computer Science. Springer (1998)

15. Sipser, M.: Introduction to the Theory of Computation, 2nd edn. Course Technology (2005)

16. [http://vlsi.colorado.edu/~fabio/ Somenzi, F.: Colorado University Decision Diagram Package].

17. Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM (2000)

18. Yuan, J., Pixley, C., Aziz, A.: Constraint-Based  Verfication. Springer (2006)

[[Категория: Совместное определение связанных терминов]]