4430
правок
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
(не показаны 4 промежуточные версии этого же участника) | |||
Строка 16: | Строка 16: | ||
'''Булевы формулы''' | '''Булевы формулы''' | ||
[[Булева формула]] определяется рекурсивным образом: [[булева переменная]] <math>x_i</math> является булевой формулой; если | [[Булева формула]] определяется рекурсивным образом: [[булева переменная]] <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-полной. Кроме того, если | [[Дизъюнкция]] представляет собой булеву формулу, содержащую только логические операции <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-полной. Кроме того, если <math>\varphi \, </math> и <math>\psi \,</math> являются ДНФ-формулами, то <math>\lnot \varphi </math> и <math>\varphi \land \psi </math> таковыми не являются, а перевод их в ДНФ, представляющие ту же функцию, может привести к экспоненциальному росту размера формулы. | ||
'''Деревья Шеннона''' | '''Деревья Шеннона''' | ||
Строка 46: | Строка 46: | ||
Определение изоморфизма напрямую дает нам рекурсивный алгоритм проверки на изоморфизм. Однако он имеет экспоненциальную по отношению к числу узлов сложность; это можно проиллюстрировать, в частности, при помощи проверки изоморфизма БДР для функции четности относительно ее самой. Экспоненциальная сложность связана с постоянно возникающими проверками на изоморфизм между парами вершин; решение может быть найдено в динамическом программировании. Кэширование проверок на изоморфизм снижает сложность этих проверок до O(|F| <math>\cdot </math> |G|), где |B| обозначает количество вершин в БДР B. | Определение изоморфизма напрямую дает нам рекурсивный алгоритм проверки на изоморфизм. Однако он имеет экспоненциальную по отношению к числу узлов сложность; это можно проиллюстрировать, в частности, при помощи проверки изоморфизма БДР для функции четности относительно ее самой. Экспоненциальная сложность связана с постоянно возникающими проверками на изоморфизм между парами вершин; решение может быть найдено в динамическом программировании. Кэширование проверок на изоморфизм снижает сложность этих проверок до 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, которая вычисляет БДР, представляющую логическое сложение AND функций, представленных двумя БДР, bdd_or и bdd_not определяются аналогичным образом для OR и NOT; bdd_compose принимает БДР, представляющие функции f и g, и переменную v и возвращает БДР для f, в которой v заменена на g. | ||
Пример bdd_and был выбран не случайно: он основан на тождестве f | |||
Пример 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|). | Реализация bdd_and вышеописанным способом имеет экспоненциальную сложность из-за постоянного возникновения новых подзадач. Динамическое программирование вновь может стать вариантом решения этой проблемы: кэширование промежуточных результатов bdd_and снижает сложность до O(|F| • |G|). | ||
'''Упорядочение переменных''' | '''Упорядочение переменных''' | ||
Строка 59: | Строка 63: | ||
== Применение == | == Применение == | ||
БДР чаще всего применяются в контексте формальной верификации цифрового оборудования [8]. Цифровое оборудование является расширением понятия схемы, описанного выше, путем введения элементов хранения состояния, которые хранят булево значение между обновлениями и обновляются по сигналу синхронизатора. | БДР чаще всего применяются в контексте формальной верификации цифрового оборудования [8]. Цифровое оборудование является расширением понятия схемы, описанного выше, путем введения элементов хранения состояния, которые хранят булево значение между обновлениями и обновляются по сигналу синхронизатора. | ||
Вентили, составляющие конструкцию, часто обновляются в силу эксплуатационных требований; эти изменения обычно не предполагают изменения логической функциональности конструкции. Подходы, основанные на использовании БДР, применяются для проверки эквивалентности при проектировании цифрового оборудования [10]. | Вентили, составляющие конструкцию, часто обновляются в силу эксплуатационных требований; эти изменения обычно не предполагают изменения логической функциональности конструкции. Подходы, основанные на использовании БДР, применяются для проверки эквивалентности при проектировании цифрового оборудования [10]. | ||
БДР также используются для проверки свойств цифрового оборудования. Типичная формулировка выглядит следующим образом: имеются множество «хороших» состояний и множество «начальных» состояний, определенные при помощи булевых формул над элементами хранения состояния; свойство выполняется в том и только том случае, если не имеется последовательностей входных значений, которые приводят состояние в начальном состоянии в состояние, не входящее в множество хороших состояний. Если имеется конструкция с n регистрами, множество состояний A в конструкции может быть охарактеризовано формулой | |||
Бинарные диаграммы решений использовались также для генерации тестов. Один из подходов к генерации тестов заключается в задании допустимых входных значений при помощи ограничений, которые, в сущности, являются булевыми формулами над первичным входом и переменными состояния. Юань и коллеги [18] продемонстрировали высокую эффективность БДР в работе с подобными ограничениями. | БДР также используются для проверки свойств цифрового оборудования. Типичная формулировка выглядит следующим образом: имеются множество «хороших» состояний и множество «начальных» состояний, определенные при помощи булевых формул над элементами хранения состояния; свойство выполняется в том и только том случае, если не имеется последовательностей входных значений, которые приводят состояние в начальном состоянии в состояние, не входящее в множество хороших состояний. Если имеется конструкция с 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 минут. При этом он использовал выведенное вручную упорядочение. | Брайант исследовал возможность проверки двух качественно различных схем для сложения. Ему удалось проверить эквивалентность двух 64-битных сумматоров на VAX 11/780 (компьютере с одним MIP) за 95,8 минут. При этом он использовал выведенное вручную упорядочение. | ||
Современные БДР-пакеты работают на два порядка величины быстрее, чем первая реализация Брайанта. Одним из источников усовершенствования было использование строгой канонической формы, в которой поддерживается глобальная база данных вершин БДР, и ни одна новая вершина не может быть добавлена без проверки, не существует ли уже в базе данных вершины с той же меткой и теми же 0-потомком и 1-потомком [3]. (Для этого требуется, чтобы потомки любой добавляемой вершины также находились в строгой канонической форме). Другими путями к повышению производительности были использование дополнительных указателей (если у указателя установлен наименьший значащий бит, он ссылается на дополнение функции), лучшее управление памятью (сборка мусора на базе счетчиков ссылок, хранение часто используемых вершин в памяти поблизости друг от друга), улучшенные хэш-функции и лучшая организация таблицы вычисленных результатов (в которой отслеживаются подзадачи, уже встреченные ранее) [16]. | |||
Современные БДР-пакеты работают на два порядка величины быстрее, чем первая реализация Брайанта. Одним из источников усовершенствования было использование [[строгая каноническая форма|строгой канонической формы]], в которой поддерживается глобальная база данных вершин БДР, и ни одна новая вершина не может быть добавлена без проверки, не существует ли уже в базе данных вершины с той же меткой и теми же 0-потомком и 1-потомком [3]. (Для этого требуется, чтобы потомки любой добавляемой вершины также находились в строгой канонической форме). Другими путями к повышению производительности были использование дополнительных указателей (если у указателя установлен наименьший значащий бит, он ссылается на дополнение функции), лучшее управление памятью (сборка мусора на базе счетчиков ссылок, хранение часто используемых вершин в памяти поблизости друг от друга), улучшенные хэш-функции и лучшая организация таблицы вычисленных результатов (в которой отслеживаются подзадачи, уже встреченные ранее) [16]. | |||
'''Наборы данных''' | '''Наборы данных''' |
правок