Параллельная технология решения SAT-задач и ее реализация в виде пакета прикладных программ

• Автор: Заикин, Олег Сергеевич
• Шифр специальности: 05.13.01
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Иркутск
• Количество страниц: 117 с. : ил.

Оглавление
Введение.

Глава 1. 8АТзадачи и основные технологии, используемые при их решении

1.1. Постановка БАТзадач. Сведение задач обращения дискретных функций

к БАТзадачам

1.2. Методы и алгоритмы решения БАТзадач

1.3. Области применения БАТзадач

Глава 2. Технология крупноблочного параллелизма в решении 8АТзадач

2.1. Методы параллельного решения 8АТзадач

2.2. Крупноблочный параллелизм в 8АТзадачах.

2.3. Прогнозирование времени параллельного решения БАТзадач.

2.4. Схемы формирования декомпозиционных множеств
Глава 3. Пакет прикладных программ ИБАТ и вычислительные эксперименты.
3.1. Описание пакета прикладных программ ИБАТ.
3.1.1. Библиотека программ пакега ББАТ
3.1.2. Режимы работы пакета ЭБАТ
3.1.3. Дополнительные аспекты пакета ББАТ.
3.2. Параллельный логический криптоанализ некоторых генераторов ключевого потока.
3.2.1. Особенности пропозиционального кодирования генераторов ключевого потока.
3.2.1. Криптоанализ генератора Гиффорда
3.2.2. Криптоанализ суммирующего генератора
3.2.3. Криптоанализ порогового генератора
3.2.4. Прогнозирование трудоемкости параллельного логического криптоанализа генератора А51
Заключение
Список использованной литературы


Работа состоит из введения, 3-х глав, заключения и списка литерату ры. В перво»! АТ-подход к решению задач обращения дискретных функций. SAT-рсшателей. Описана концепция логического криптоанализа. В разделе 1. Задача обращения дискретной функции семейства 3 ставится следующим образом: по известному образу найти хотя бы один прообраз. Проблемы обращения функций произвольного семейства из класса 3 допускают эффективную сводимость к проблемам поиска решений логических уравнений вида «КНФ=1», где КНФ - это конъюнктивная нормальная форма над некоторым множеством булевых переменных. Задачи поиска решений таких уравнений называются SAT-задачами. В разделе 1. SAT-решателей (программных комплексов, решающих SAT-задачи), основанных на алгоритме DPLL. Приведен обзор следующих базовых технологий, используемых в такого рода SAT-решатслях: бэктрекинг, нехроиологический бэктрекинг, правило единичного дизъюнкта, ВСР-стратегия, процедура «Clause Learning», процедуры чистки базы ограничений, рестарты. В разделе 1. SAT-задача). В отношении генераторов ключевого потока приводится постановка логического криптоанализа как задачи обращения дискретных функция из класса 3. Во второй главе описана параллельная технология решения SAT-задач. Предложены различные виды декомпозиционных представлений и описана процедура прогнозирования трудоемкости параллельного решения SAT-задач. В разделе 2. АТ-задач. В разделе 2. АТ-задач. Общая идея данной методики состоит в следующем. Рассматривается произвольная КНФ (называемая далее исходной) над множеством булевых переменных X. Декомпозиционным множеством называется некоторое подмножество Xх множества X. Декомпозиционному множеству х' ставится в соответствие множество у(х')={ги. Ук}у состоящее из к = 2л различных двоичных векторов, каждый из которых является вектором значений переменных из Xх. КНФ из декомпозиционного семейства. Наоборот, произвольному набору, выполняющему некоторую КНФ из декомпозиционного семейства, соответствует единственный набор, выполняющий исходную КНФ. Таким образом, БАТ-задача относительно исходной КНФ сводится к решению 8АТ-задач для КНФ из декомпозиционного семейства. В разделе 2. ЭАТ-задач при их крупноблочном распараллеливании. Предположим, что зафиксировано некоторое декомпозиционное множество Xх. Представляет интерес «улучшение» Xх, то есть построение такого подмножества Xх, использование которого в качестве декомпозиционного множества делают декомпозицию более эффективной, чем на основе Xх. SAT-задач для серии КНФ, выбранных случайным образом из декомпозиционного множества. Введена специальная прогнозная функция и задача выбора оптимального (по прогнозу) декомпозиционного множества решается через задачу оптимизации данной функции. В разделе 2. Основой данной методики является понятие схемы формирования декомпозиционного множества (далее «схема формирования»). Схема формирования - это алгоритм построения декомпозиционных множеств заданной мощности. Здесь же предлагается совмещение технологии статистического прогнозирования с использованием различных схем формирования. При этом каждой схеме формирования ставится в соответствие прогноз трудоемкости параллельного вычисления, после чего выбирается схема формирования и соответствующая декомпозиция, дающие на и лучшие прогнозные значения. В третьей главе приведено описание пакета прикладных программ (ППП) D-SAT1 (созданного для реализации параллельной технологии, предложенной во второй главе), а также результаты вычислительных экспериментов. В разделе 3. ППП D-SAT. ГТП D-SAT функционирует в РВС под управлением инструментального комплекса Distributed Computing system of Modular Programming (D1SCOMP2). Библиотека программ ППП D-SAT включает модуль расщепления, модуль SAT-решателя, модуль прогнозирования, модуль сравнения, аналитический модуль и транспортный модуль. Занкин О. С. Пакет прикладных программ Distributed-SAT: Свидетельство об официальной регистрации программы для ЭВМ № . М.: Федеральная служба но интеллектуальной собственности, патентам и товарным знакам, . Разработчик Сидоров И.