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

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

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

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

Том:

Номер: 1 (7)

Год: 2010

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

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

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

URL:

Проекты:

DOI:

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

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

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

Индексируется УБС: Нет

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

Индексируется ВАК: Нет

Индексируется CORE: Нет

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