Бинарный граф решений: различия между версиями

[[Булева формула]] определяется рекурсивным образом: [[булева переменная]] <math>x_i</math> является булевой формулой; если φ и ψ являются булевыми формулами, то ими являются также (<math>\lnot</math>φ), (φ <math>\land</math> ψ), (φ <math>\lor</math> ψ), (φ <math>\rightarrow</math> ψ) и (φ <math>\leftrightarrow</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].

Дизъюнкция представляет собой булеву формулу, содержащую только логические операции  и , причем  применяется только к переменным; к примеру, x1   x3  x5 является дизъюнкцией. Булева формула находится в дизъюнктивной нормальной форме (ДНФ), если она имеет вид D0  D1  …  Dk-1, где каждый член Di является дизъюнкцией. ДНФ-формулы могут представлять произвольные булевы функции, например, путем определения каждого входа, на котором формула принимает значение 1, как дизъюнкции. ДНФ-формулы применяются в проектировании логических схем, поскольку могут быть непосредственно переведены в ПЛМ [4]. Однако если проблема выполнимости ДНФ-формул решается тривиально, то проблема эквивалентности является NP-полной. Кроме того, если φ и ψ являются ДНФ-формулами, то φ и φ  ψ таковыми не являются, а перевод их в ДНФ, представляющие ту же функцию, может привести к экспоненциальному росту размера формулы.

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

fxi(α0, ... ,αi-1, ai, αi+1, …, αn-1) = f(α0, ... ,αi-1, 1, αi+1, …, αn-1).

Отрицательный сомножитель относительно xi, обозначаемый fxi’ определяется точно так же, только на правой стороне вместо 1 стоит 0.

f(x1, ... , xn) = xi • fxi + x'i fx’i

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

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

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

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

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

Пример bdd_and был выбран не случайно: он основан на тождестве f • g = x • (fx • gx) + x’ • (fx’ • gx’). Рекурсия может быть реализована напрямую: основными являются ситуации, когда либо f, либо g равны 0, и когда одно или оба значения равны 1. Рекурсивный процесс выбирает переменную v, являющуюся меткой корня БДР либо для f, либо для g, в зависимости от того, что из них идет раньше по порядку переменных, и, рекурсивно вычисляет БДР для fv • gv и fv' • gv'; если они изоморфны, выполняется их слияние. Пусть дана БДР F для f. Если v – переменная, служащая меткой корня F, то БДР для fv’ и fv представляют собой просто 0-потомка и 1-потомка корня F, соответственно.

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

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

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