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

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

Тип публикации: Статья в журнале

Тип материала: Текст

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

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

Язык публикации: russian

Номера страниц: 86-104

Количество страниц: 19

Номер: 1 (7)

Год публикации: 2010

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

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

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

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

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

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

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

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