Методы обращения дискретных функций с применением двоичных решающих диаграмм

• Автор: Игнатьев, Алексей Сергеевич
• Шифр специальности: 05.13.18
• Научная степень: Кандидатская
• Год защиты: 2010
• Место защиты: Иркутск
• Количество страниц: 110 с. : ил.

Содержание
Введение .

Глава 1. Дискретные функции, логические уравнения и двоичные диаграммы решений

1.1. Общие сведения из теории булевых функций. Логические

уравнения .

1.2. Э АТподход к задачам обращения дискретных функций краткое описание

1.2.1. Основа БАТподхода.

1.2.2. Основные алгоритмы решения БАТзадач.

1.3. Двоичные решающие диаграммы.

1.3.1. Базовые понятия

1.3.2. Основные алгоритмы работы с ВББ

Глава 2. Алгоритмы решения логических уравнений и обращения дискретных функций, использующие
2.1. Алгоригмика ИОВЕЮиодхода к решению систем логических
уравнений .
2.1.1. Специальные представления формул ИВ
2.1.2. Разбиение системы на слои и использование шаблонов
2.2. Процедуры изменения порядка означивания переменных в
ПО В ОБ
2.3. Основы гибридного БАТ ЯОВББ подхода к задачам обращения дискретных функций.
2.4. Логический вывод на 1ЮВББ основные алгоритмы
Глава 3. Реализация и тестирование параллельных алгоритмов обращения дискретных функций, использующих ЕШ1
3.1. Реализация и тестирование ГЮВООрешателя логических
уравнений .
3.1.1. Базовые структуры данных.
3.1.2. Организация работы с памятью при работе ЛОВИИ
3.1.3. Применение ИОВОЮрешателя логических уравнений к исследованию дискретноавтоматных моделей генных сетей
3.2. Параллельная реализация гибридного БАТ0ВООподхода
к решению задач обращения дискретных функций
3.2.1. Реализация и тестирование последовательного гибридного БАТН.ОВИИрешателя
3.2.2. Реализация и тестирование параллельного гибридного БАТЬ0 ВИИрешателя, функционирующего в МР1среде.
Заключение
Литература


ROBDD представлений соответствующих булевых функций (данный шаг предполагает сокращение объема оперативной памяти, используемой для храпения накопленных ограничений); разработать и реализовать ROBDD-аналоги основных механизмов вывода, используемых в современных SAT-решателях; строго обосновать корректность и эффективность работы соответствующих процедур. Разработать и программно реализовать ROBDD-решатель систем логических уравнений, использующий новые эвристические алгоритмы. Программно реализовать гибридный (SATH-ROBDD)-pemaTejib логических уравнений, ориентированный на задачи обращения полиномиально вычислимых дискретных функций; разработать параллельные гибридные (SAT-f-ROBDD)-ajiropHTMbi решения логических уравнений и обращения дискретных функций; программно реализовать разработанные алгоритмы с использованием стандарта MPI (Message Passing Interface); интегрировать все разработанные алгоритмы в программный комплекс. Протестировать построенный программный комплекс на задачах обращения криптографических функций и задачах исследования некоторых автоматных моделей. Методы и инструменты исследования. Теоретическая часть исследования использует аппарат теории множеств, дискретной математики, теории вычислительной сложности, теории булевых функций, теории параллельных вычислений, а экспериментальная — современные средства разработки программного обеспечения, а также многопроцессорные вычислительные системы. Научная новизна. Основные результаты, выносимые на защиту. Метод обращения полиномиально вычислимых дискретных функций, в основе которого лежит гибридный (SAT-fROBDD) логический вывод; строгое обоснование (в форме теорем) математических свойств ROBDD, рассматриваемых в роли баз булевых ограничений; ROBDD-аналоги основных процедур, используемых в нехронологическом DPLL-выводе (правило единичного . Clause Learning», процедуры работы с дизъюнктами, использующие идеологию «отсроченных вычислений»). Новые эвристические алгоритмы решения систем логических уравнений, использующие двоичные решающие диаграммы (ROBDD). Программный комплекс, представляющий собой новый гибридный (SAT-fR. OBDD)-решатель, ориентированный на решение задач обращения дискретных функций и функционирующий в распределенных вычислительных средах (РВС). РВС. Достоверность результатов. Достоверность порученных в работе теоретических результатов обеспечивается строгостью производимых математических построений. Корректность алгоритмов и эффективность их практической реализации подтверждаются результатами вычислительных экспериментов. Соответствие специальности. В диссертации разработан новый вычислительный метод, использующий алгоритмы обработки дискретных данных и применимый к широкому спектру практических задач (тестирование и верификация дискретных управляющих систем, исследование различных дискретно-автоматных моделей, обращение дискретных функций, криптоанализ). Разработанный метод реализован в виде программного комплекса, функционирующего в распределенных вычислительных средах. Комплекс протестирован на аргументированно трудных задачах обращения некоторых криптографических функций. Теоретическая и практическая значимость работы. Теоретическая значимость работы заключена в возможности применения предложенных методов к исследованию алгоритмических аспектов задач обращения дискретных функций. Практическая значимость состоит в возможности использовать предложенные методы и применяемые в них вычислительные алгоритмы в исследовании широкого класса моделей дискретных систем, поведение которых описывается полиномиально вычислимыми дискретными функциями. Содержательная часть работы включает введение и три главы. Первая глава является обзорной и содержит теоретическую базу для последующего материала. В данной главе приведены необходимые сведения из теории дискретных функций, кратко описаны основные алгоритмы решения БАТ-задач. Заключительный раздел первой главы посвящен основам теории двоичных решающих диаграмм и их применению к логическим уравнениям и задачам обращения дискретных функций.