|
Прикладная дискретная математика, 2010, номер 1(7), страницы 86–104
(Mi pdm164)
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье)
Вычислительные методы в дискретной математике
Алгоритмы работы с ROBDD как с базами булевых ограничений
А. С. Игнатьев, А. А. Семенов Институт динамики систем и теории управления СО РАН, г. Иркутск, Россия
Аннотация:
Исследуются алгоритмические свойства сокращенных упорядоченных диаграмм решений (ROBDD) при их рассмотрении в роли баз булевых ограничений в гибридном (SAT+ROBDD)-выводе. Приведены ROBDD-аналоги основных алгоритмических процедур, используемых в DPLL-выводе (подстановки, правило единичного дизъюнкта, CL-процедура, механизмы отсроченных вычислений). Описан новый алгоритм изменения порядка в ROBDD. Для всех алгоритмов приводятся оценки их трудоемкости.
Ключевые слова:
логические уравнения, двоичные диаграммы решений, гибридный вывод.
Образец цитирования:
А. С. Игнатьев, А. А. Семенов, “Алгоритмы работы с ROBDD как с базами булевых ограничений”, ПДМ, 2010, № 1(7), 86–104
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/pdm164 https://www.mathnet.ru/rus/pdm/y2010/i1/p86
|
Статистика просмотров: |
Страница аннотации: | 471 | PDF полного текста: | 253 | Список литературы: | 56 |
|