Страница публикации

Алгоритмы работы с ROBDD как с базами булевых ограничений

Авторы: Игнатьев А.С., Семенов А.А.

Журнал: Прикладная дискретная математика

Том:

Номер: 1 (7)

Год: 2010

Отчётный год: 2010

Издательство:

Местоположение издательства:

URL:

Аннотация: Исследуются алгоритмические свойства сокращенных упорядоченных диаграмм решений (ROBDD) при их рассмотрении в роли баз булевых ограничений в гибридном (SAT+ROBDD)-выводе. Приведены ROBDD-аналоги основных алгоритмических процедур, используемых в DPLL-выводе (подстановки, правило единичного дизъюнкта, CL-процедура, механизмы отсроченных вычислений). Описан новый алгоритм изменения порядка в ROBDD. Для всех алгоритмов приводятся оценки их трудоемкости.

Индексируется WOS: 0

Индексируется Scopus: 0

Индексируется РИНЦ: 1

Публикация в печати: 0

Добавил в систему: