автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.01, диссертация на тему:Параллельная технология решения SAT-задач и ее реализация в виде пакета прикладных программ

На правах рукописи

Заикин Олег Сергеевич

ПАРАЛЛЕЛЬНАЯ ТЕХНОЛОГИЯ РЕШЕНИЯ вАТ-ЗАДАЧ И ЕЕ РЕАЛИЗАЦИЯ В ВИДЕ ПАКЕТА ПРИКЛАДНЫХ ПРОГРАММ

05.13.01 - Системный анализ, управление и обработка информации (в отраслях информатики, вычислительной техники и автоматизации)

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

Томск - 2009

003459660

Работа выполнена в Институте динамики систем и теории управления СО РАН. Научный руководитель:

кандидат технических наук Семенов Александр Анатольевич

Официальные оппоненты:

доктор физико-математических наук,

профессор Корольков Юрий Дмитриевич

кандидат технических наук Тимошевская Наталия Евгеньевна

Ведущая организация:

Институт вычислительного моделирования СО РАН (г. Красноярск) Зашита состоится:

22 января 2008 г. в 10.30 на заседании Диссертационного совета Д 212.267.12 при ГОУ ВПО «Томский государственный университет» по адресу: 634050, г. Томск, пр. Ленина, 36.

С диссертацией можно ознакомиться:

В научной библиотеке Томского государственного университета. Автореферат разослан 21 декабря 2008 г.

Ученый секретарь диссертационного совета,

д.т.н., профессор ( СмагинВ. И.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность работы

Многие значимые в практическом отношении проблемы, связанные с управлением и обработкой информации в дискретных системах, допускают эффективные сводимости к задачам поиска решений логических уравнений. Сказанное касается проблем синтеза и верификации в микроэлектронике, целого ряда вопросов теоретического программирования, задач обращения дискретных функций, задач управления коммуникационными протоколами и многих других. Один из наиболее важных классов логических уравнений образован уравнениями вида «КНФ = 1» (КНФ - конъюнктивная нормальная форма). Задачи поиска решений данного класса уравнений относятся к так называемым «БАТ-задачам». Для решения БАТ-задач используются специальные программные комплексы, называемые БАТ-решателями. В построении БАТ-решателей в последние годы отмечен реальный прогресс.

Высокая вычислительная сложность БАТ-задач аргументирует использование для их решения параллельных вычислений. С этой позиции БАТ-задачи могут исследоваться по двум направлениям.

Первое направление основывается на концепции мелкозернистого параллелизма. В этом случае распараллеливание осуществляется на уровне базового алгоритма БАТ-решателя (БАТ-решатели с параллельной вычислительной архитектурой). Однако современные БАТ-решатели являются довольно сложными в структурном смысле программами, в связи с чем реализация данного подхода трудна в техническом отношении. Кроме этого, мелкозернистый параллелизм зачастую характеризуется невысокой масштабируем остыо.

В основе второго направления лежит концепция крупноблочного параллелизма. В этом случае осуществляется декомпозиция исходной ЯАТ-задачи на семейство подзадач, каждая из которых обрабатывается БАТ-решателем на отдельном вычислительном узле параллельной вычислительной системы. При этом параллельная вычислительная система свободна от ряда ограничений, присущих мелкозернистому параллелизму. Кроме этого, крупноблочный подход, как правило, характеризуется высокой масштабируемостью. Крупноблочный параллелизм предпочтителен в решении ЯАТ-задач, в которых размерность пространства полного перебора существенно меньше числа булевых переменных, фигурирующих в КНФ. Речь идет, прежде всего, о БАТ-задачах, к которым сводятся задачи обращения дискретных функций из класса, имеющего пересечения с многочисленными областями кибернетики.

Сказанное означает, что проблема создания эффективных технологий решения БАТ-задач посредством их крупноблочного распараллеливания является актуальной.

Цель работы и задачи исследования

Целью диссертационной работы является разработка и практическая реализация технологии крупноблочного распараллеливания БАТ-задач.

Для достижения указанной цели ставятся и решаются следующие основные задачи.

1. Разработка и исследование различных стратегий построения декомпозиционных представлений 8АТ-задач.

2. Разработка и алгоритмическая реализация процедуры прогнозирования трудоемкости параллельного решения 8АТ-задач.

3. Программная реализация технологии крупноблочного распараллеливания ЯАТ-задач в форме пакета прикладных программ (ППП).

4. Решение с помощью разработанного ППП БАТ-задач, кодирующих задачи обращения ряда дискретных функций, используемых в криптографии.

Методы исследования

Теоретические исследования используют аппарат теории множеств, дискретной математики, теории вычислительной сложности, параллельных вычислений, а экспериментальные - инструментальные и программные средства решения задач в параллельных вычислительных системах.

Научная новизна

Новыми являются все основные результаты, полученные в диссертации, в том числе:

- общая схема крупноблочного распараллеливания БАТ-задач;

- процедура прогнозирования трудоемкости параллельного решения БАТ-задач;

- оценка сложности процедуры прогнозирования трудоемкости параллельного решения БАТ-задач;

- разработка ППП для реализации параллельной технологии решения ЯАТ-задач;

- параллельное решение с помощью разработанного ППП вычислительно сложных БАТ-задач, кодирующих задачи обращения некоторых дискретных функций, используемых в криптографии.

При решении поставленных задач были получены перечисленные ниже вспомогательные результаты, представляющие самостоятельный интерес.

Введено понятие декомпозиционного множества; введено понятие схемы формирования семейств декомпозиционных множеств (далее «схема формирования»); введена классификация схем формирований; разработаны схемы формирования, ориентированные на структуру БАТ-задач, кодирующих задачи обращения некоторых дискретных функций; реализована процедура оптимизированной рассылки БАТ-задач, снижающая транспортные расходы в параллельных вычислительных системах.

Теоретическая и практическая значимость работы

Теоретическая значимость работы аргументируется возможностью прямого переноса ее базовых концепций на задачи дискретной оптимизации с двоичными данными. Разработанные в диссертации методы и алгоритмы могут применяться для решения широкого класса практически важных задач, допускающих эффективную сводимость к БАТ-задачам.

Достоверность результатов

Достоверность полученных в работе теоретических результатов обеспечивается строгостью производимых математических построений. Корректность и эффективность практической реализации подтверждается результатами вычислительных экспериментов.

Основные результаты, выносимые на защиту

1. Параллельная технология решения БАТ-задач, включающая общую схему крупноблочного распараллеливания БАТ-задач.

2. Разработка и анализ различных схем формирования декомпозиционных представлений БАТ-задач.

3. Процедура прогнозирования трудоемкости параллельного решения БАТ-задач; оценка сложности данной процедуры.

4. Разработка ППП для практической реализации предложенной параллельной технологии решения БАТ-задач.

5. Параллельное решение с помощью разработанного ППП вычислительно сложных БАТ-задач, кодирующих задачи обращения некоторых дискретных функций, используемых в криптографии.

Внедрение результатов исследований

Результаты диссертации внедрены:

1) в разработку технологии крупноблочного распараллеливания БАТ-задач в рамках следующих грантов РФФИ: № 04-07-90358 (2006 г.), № 07-01-00400-а (2007-2008 гг.), а также грантов поддержки ведущих научных школ: НШ-

9508.2006.1 (2006 г.), НШ-1676.2008.1 (2008 г.);

2) в создание ППП Distribuíed-SAT (D-SAT), предназначенного для параллельного решения SAT-задач: свидетельство № 2008610423 об официальной регистрации программы для ЭВМ, выданное Федеральной службой по интеллектуальной собственности, патентам и товарным знакам (2008 г.);

3) в учебный процесс (разработка курсовых и дипломных работ) Института математики, экономики и информатики Иркутского государственного университета (ИМЭИ ИГУ).

Апробация работы

Результаты диссертации докладывались и обсуждались на 1-ой и 2-ой Международных научных конференциях «Параллельные вычислительные технологии (ПАВТ)» (Челябинск, 2007; Санкт-Петербург, 2008), на 4-ой Международной конференции «Параллельные вычисления и задачи управления (РАСО'2008)» (Москва, 2008), на XV Международной конференции «Вычислительная механика и современные прикладные программные системы (ВМСППС'2007)» (Алушта, 2007), на XIV Байкальской международной школе-семинаре «Методы оптимизации и их приложения» (Северобайкальск, 2008 г.) на VI и VII Сибирских научных школах-семинарах с международным участием «Компьютерная безопасность и криптография» (Горно-Алтайск, 2007; Красноярск, 2008), на II Всероссийской конференции с международным участием «Инфокоммуникационные и вычислительные технологии и системы (ИКВТС'2006)» (Улан-Удэ, 2006), на 6-ой школе-семинаре «Распределенные и кластерные вычисления» (Красноярск, 2006), на научных конференциях «Ляпуновские чтения» (Иркутск, 2006; 2007), на VI и IX школах-семинарах молодых ученых «ММЙТ» (Иркутск, 2005; 2007); на научных семинарах Института динамики систем и теории управления СО РАН, а также на научном семинаре кафедры защиты информации и криптографии Томского государственного университета (2008 г.).

Структура работы и личный вклад автора

Диссертация состоит из введения, трех глав, заключения и списка литературы, насчитывающего 104 наименования. Объем диссертации - 116 страниц. Первая глава является обзорной, в ней отражены в основном известные результаты. Часть результатов второй главы (введение прогнозных функций, оценка сложности процедур прогнозирования времени параллельного решения SAT-задач) получены в неделимом соавторстве с научным руководителем. Все остальные результаты, представленные в диссертации, получены автором лично.

Публикации

Основные результаты диссертации опубликованы в 18 печатных работах ([1-18] в списке литературы). Работы [1] и [2] опубликованы в изданиях, входящих в список ВАК.

СОДЕРЖАНИЕ РАБОТЫ

Во введении дается общая характеристика работы, определяется тематика и цель работы, излагаются основные результаты, выносимые на защиту.

В первой главе описывается SAT-подход в решении задач обращения дискретных функций. Приведен обзор основных компонентов архитектуры современных SAT-решателей и концепция логического криптоанализа.

Рассматривается класс логических уравнений, образованный уравнениями вида с(х1,...>дгп)=1, где С(.т,,...,хя) - некоторая конъюнктивная нормальная форма (КНФ) над множеством булевых переменных X = {xt,...,xn}. Задачи решения таких уравнений называются SAT-задачами. К SAT-задачам относятся задача проверки выполнимости произвольной КНФ (исторически первая NP-полная задача) и задача поиска выполняющего набора произвольной КИФ (NP-трудная задача).

Обозначим через {ОД}" множество всех двоичных слов длины п, {0,1}' = U„fN{0>l}" ' Дискретной функцией называется произвольная функция вида fn: {0,l}" -» {0,l}*. Через dorn /„ с {0,l}" обозначается область определения функции /„, а через range fn с {ОД}* - ее область значений. Дискретную функцию f„ назовем всюду определенной, если dorn fn = {o,l}". Семейство всюду определенных дискретных функций, вычислимых некоторой программой машины Тьюринга, обозначается через / = {fn }/icN . Класс 3 образован всеми

алгоритмически вычислимыми за полиномиальное от п время всюду определенными семействами дискретных функций. Задача обращения дискретной функции /п семейства /еЗ ставится следующим образом: дано

двоичное слово у е range fn, требуется найти такое слово х е {ОД}", что

В работе1 было предложено (со ссылками на результаты С.А. Кука) рассматривать проблемы обращения функций произвольного семейства

/е3 как задачи поиска решений логических уравнений вида C(xt,...,x (п)) = 1,

где /?(•) - некоторый полином, a C(xv...,x p(fi)) - КНФ над множеством булевых

переменных X = [г,,...,хр(п)|. Функция объема получаемого при этом семейства

КНФ есть некоторый полином от п.

Функция объема получаемого при этом семейства КНФ есть некоторый полином от л.

Консервативность сведения исходного уравнения к уравнению вида С{хи...,хр(п)) = 1 означает равномощность множеств решений этих уравнений.

В настоящее время известны консервативные процедуры сведения задач обращения дискретных функций из класса 3 к SAT-задачам. В основе данных процедур лежат преобразования Цейтина.

В соответствии с перечисленными результатами общая концепция SAT-подхода в решении задач обращения дискретных функций состоит в следующем.

- Алгоритм вычисления произвольной функции /„ семейства

/ = {/„}n6N,/e 3, консервативно преобразуется в уравнение вида С(х1,...,хр^1-)) = I.

- В уравнение С(х1,...,хр(п)) = 1 подставляется известный вектор у е range /„.

- Полученная в результате КНФ С является выполнимой, а из выполняющего ее набора можно выделить компоненты вектора х е {0,1}" такого,

что /„(*)=У ■

Тем самым задача обращения функции /л в точке yerangefn оказывается сведенной к SAT-задаче.

Для решения SAT-задач используются специальные программные комплексы, называемые SAT-решателями. Большая часть эффективных (по результатам специализированных конкурсов) SAT-решателей использует в

1 Заикин О.С., Семенов A.A. Технология крупноблочного параллелизма в SAT-задачах II Проблемы управления. - 2008. - №1. с. 43-50.

качестве основы алгоритм ОРЬЬ. Пусть С^,...,*„) - произвольная КНФ над множеством булевых переменных X = {*[,...,хп}. В основе ЭРЬЬ лежит процедура итеративного означивания переменных из X в некотором порядке с последующей подстановкой значений в С(х1,...,хп). Данная процедура представляется в форме двоичного дерева. При этом вершины дерева интерпретируют выбор соответствующих булевых переменных, ветви дерева интерпретируют присвоения этим переменным значений истинности, а листья дерева интерпретируют значения булевой функции С(х,,...,х„) при соответствующем означивании переменных из X. Приведенная процедура в БР1Х дополнена отслеживанием возможности срабатывания правила единичного дизъюнкта. Схема подстановок в КНФ значений переменных с последующим срабатыванием правила единичного дизъюнкта называется стратегией распространения булевых ограничений (ВСР-стратегия). Помимо перечисленного современные БАТ-решатели, основанные на БРЬЬ, используют различные технологии, позволяющие ускорять поиск (нехронологический бэктрекинг, процедура запоминания информации о конфликтах, рестарты, быстрые структуры данных и др.).

В диссертации в основном рассматриваются БАТ-задачи, полученные в результате сведения к ним криптографических задач из области поточного шифрования. Этот выбор обусловлен потребностью в аргументировано сложных тестах. Большинство используемых на практике поточных шифров относится к двоичным аддитивным. В таких шифрах на основе секретного ключа с помощью генераторов ключевого потока (делее — генератора) порождается ключевой поток, а шифртекст образуется путем сложения исходного текста по модулю 2 с ключевым потоком. Входная последовательность генератора называется инициализирующей.

Генератор можно рассматривать как семейство дискретных функций

й = {¿Г,,},,^ вида £„ :{0Д}"->{0,1}\ яеЫ, яеЗ. Алгоритм вычисления функций называется порождающим алгоритмом генератора. Под

криптоанализом генератора понимается поиск инициализирующей последовательности х = (х^,...,хп) по известному фрагменту у ключевого потока. Криптоанализ, рассматриваемый как БАТ-задача, называется логическим криптоанализом. Обозначим через С° КНФ, полученную в результате пропозиционального кодирования алгоритма, реализующего g. КНФ,

получаемую в результате подстановки в С° значений переменных, кодирующих

ключевой поток, обозначим через С*. Тем самым задача поиска инициализирующей последовательности генератора g оказывается сведенной к БАТ-задаче.

Во второй главе описана технология крупноблочного распараллеливания БАТ-задач. Рассмотрены различные виды декомпозиционных представлений, и описана процедура прогнозирования трудоемкости параллельного решения БАТ-задач.

Распределенная вычислительная среда (далее РВС) - совокупность вычислительных узлов, объединенных коммуникационной сетью. Вычислительный узел РВС - программно-аппаратный ресурс, включающий аппаратное и программное обеспечение, требуемое для решения одно или нескольких вычислительных задач. Вычислительный кластер (далее кластер) -совокупность вычислительных узлов РВС, объединенных единой коммуникационной средой. Главный (управляющий) узел РВС - один из вычислительных узлов РВС, обладающий функциями управления заданиями пользователей и ресурсами РВС.

Ниже приведено описание основных элементов разработанной в диссертации технологии крупноблочного распараллеливания БАТ-задач.

Рассматривается произвольная КНФ С над множеством булевых переменных X = {л,,...,^}. Выбираем в множестве X некоторое подмножество

Х'= ^ }, 0\......-.4 Л е {1,...,л}.

Назовем множество Х'= } декомпозиционным множеством, & <1

- размерностью декомпозиционного множества. Дополнительно полагаем, что при й = 0 декомпозиционное множество пусто. Декомпозиционному множеству Х':\Х'\=с1,(1>0 поставим в соответствие множество 7(Л") = {к,,...,^},

состоящее из к = различных двоичных векторов длины й, каждый из которых является вектором значений переменных х^ . Декомпозиционным

семейством, порожденным из КНФ С множеством Xх, называется множество Ад.,(с) КНФ, полученных подстановками в С векторов е {1,...Д}:

д^сИс^с^.А =су, Л0(с)={с}.

Несложно видеть, что любой набор а е {о,1}", выполняющий С ( С |я = 1), в компонентах, входящих в X', совпадает с некоторым вектором Vх е У(Х'), а в остальных компонентах совпадает с набором, выполняющим КНФ

С \r„ е Лх,(с). КНФ С при этом невыполнима тогда и только тогда, когда все КНФ в Ax,(c) невыполнимы. Таким образом, SAT-задача относительно исходной КНФ С сводится к решению к SAT-задач для КНФ из множества Ах (с). Для обработки множества Д Г(С') может быть использована РВС.

Предположим, что зафиксировано некоторое декомпозиционное множество Х',\ Х'\- d. В силу сказанного выше, исходная SAT-задача сводится

к решению 2d SAT задач для КНФ из множества Ах (с). Следующий вопрос

сострит в том, можно ли в X' выбрать подмножество Х~, декомпозиция на основе которого была бы существенно эффективнее, чем на основе Х"1 В работе2 была предложена специальная процедура статистического прогнозирования, предназначенная для улучшения декомпозиционного множества. Краткое описание данной процедуры приведено ниже.

Введем в рассмотрение натуральное число R0, предназначением которого является разделение ситуаций - когда имеется необходимость формирования случайной выборки, и когда такой необходимости нет. Например, за R^ можно принять число, близкое к числу процессоров в кластере. Если при некотором Х~ с X', | Х~ |= d мощность семейства А^,_(с) слишком велика, то

представление о времени соответствующего параллельного вычисления можно составить на основе знания среднего времени решения SAT-задач для серии КНФ, выбранных случайным образом из А (С).

Через qd обозначаем объем такой выборки. Через Yd обозначается множество, образованное всеми различными векторами значений переменных из X~:\X~\=d. Каждому значению параметра dе{0,1,...,|Х'\} такому, что 2d >R0, ставится в соответствие множество векторов |, выбираемых

из Yd в соответствии с равномерным распределением, а также множество выборка) КНФ ©rf = jCyi =С \г. ]. Каждому значению параметра

с/е{0,1,...,|^'|} такому, что 2d <R0, ставится в соответствие множество Yd и

Заикин О.С., Семенов A.A. Технология крупноблочного параллелизма в SAT-адачах // Проблемы управления. - 2008. - №1. С. 43-50.

множество КНФ ©rf=jc, =Cly¡,...,C2¿ =C\Yj ] (в данном случае Qd =Ай(С)). Множество выборок {©rf г Jr!i далее обозначаем через 0.

Фиксируем некоторый SAT-решатель S. Обозначим через t(C') время работы (число битовых операций) SAT-решателя S на произвольном входе С". Введем в рассмотрение функцию ts : © N,

Значением данной функции при каждом фиксированном d е {o,l,...,j X'l} является суммарное время (число битовых операций) работы SAT-решателя S по всем КНФ из ©¿. Следует учитывать, что при некоторых значениях параметра d (например, при d = 0) КНФ из ®d могут оказаться очень сложными для SAT-решателя, и в этом случае время подсчета соответствующего значения прогнозной функции может превысить разумные границы. Для учета данного факта вводится в рассмотрение специальная функция g(c)=p(m-n), здесь т - число дизъюнктов в КНФ С, а р(-) - некоторый полином, степень которого больше 1. Допустим, что в соответствии с перечисленными правилами построено семейство выборок © = {©«/}d£(oi ¡a-d (пРи фиксированном /?0). Прогнозную функцию определим следующим образом.

— ■vs{Qd\2d>Rü,ts{Qi)<g{Cy, co,rs(0,)>g(C).

Запись «T(&d) = ос » означает, что функция не определена на выборке Qd . Рациональное число T{®d) является прогнозом общего объема битовых операций, требуемого для решения исходной SAT-задачи при декомпозиции КНФ С на семейство КНФ, порожденное множеством Xa . Тем самым задача прогнозного планирования оптимального по трудоемкости параллельного вычисления сводится к задаче минимизации функции Т на множестве domT с 0.

Во второй главе диссертации приводится алгоритм типа «динамического программирования» полиномиальной трудоемкости, позволяющий решать описанную задачу минимизации для одного класса прогнозных функций.

Далее приведено описание общей процедуры крупноблочного распараллеливания БАТ-задачи с последующим решением полученного семейства БАТ-задач в РВС. Параметры декомпозиции исходной БАТ-задачи определяются на основе знания глобального минимума прогнозной функции Т на множестве &отТ.

Пусть Х7 (ХГ сГ, ] Х^ | = </ ) - это такое множество, что (с/*,)) -точка глобального минимума функции Т на области ее определения. Пусть Л*(с)= {С1;..., СА}, к-2а , - декомпозиционное семейство КНФ, порожденное из С множеством XГ. Пусть имеется РВС, состоящая из г вычислительных узлов, где г е N. Возможны следующие два случая.

1) к<г, то есть число КНФ в семействе Л*(с) не превосходит числа вычислительных узлов РВС. В этом случае для каждой КНФ из семейства Л'(с) БАТ-задача решается на отдельном вычислительном узле РВС. На практике такая ситуация возникает весьма редко.

2) к>г — число КНФ в семействе Л*(с) больше числа вычислительных узлов РВС. Именно такая ситуация наиболее типична для задач обращения криптографических функций из 3. В данном случае каждому вектору

У} е е{1,к = 2а , ставится в соответствие натуральное число (назовем его натуральным индексом КНФ С)), двоичным представлением которого является вектор У^. Пусть КНФ семейства Л*(с) упорядочены некоторым образом (например, по возрастанию их натуральных индексов). Произвольную КНФ из Д*(с) назовем связанной, если в рассматриваемый момент времени БАТ-задача для нее либо уже решена, либо решается на некотором вычислительном узле РВС. Остальные КНФ называем свободными. Выбираются первые г КНФ СХ,...,СГ из семейства Д*(с). Для каждой из выбранных КНФ С,,...,С, решается БАТ-задача на отдельном вычислительном узле РВС. Как только освобождается некоторый из г вычислительных узлов РВС, на нем запускается процедура решения БАТ-задачи для первой (в смысле введенного выше порядка) свободной КНФ семейства Л*(с). Данный процесс продолжается

до тех пор, пока не будет найден выполняющий набор некоторой КНФ из Д*(с), либо пока не будет доказана невыполнимость всех КНФ из Л*(с). В силу сказанного выше данная процедура решает SAT-задачу для произвольной КНФ С корректно.

Отметим, что рассмотренная выше процедура использовала фиксированное некоторым (неопределенным) образом множество X'. Во второй главе диссертации предлагается общая методика построения декомпозиционных множеств. Основой данной методики является понятие схемы формирования декомпозиционного множества.

Схемой формирования семейства декомпозиционных множеств (далее «схема формирования») назовем семейство Н = {h0,...,hn} отображений множества булевых переменных X = {хи...,хп] в семейство множеств \Хц,...,Хпн}, где XdH,dе{0,..., п}, - декомпозиционное множество размерности d, hd:X-> X*,, d е {(),...,«}. При этом для любого Я полагается, что Х°„ = 0.

Одним из результатов второй главы диссертации является совмещение технологии прогнозных функций с использованием различных схем формирования. При этом каждой схеме формирования Н ставится в соответствие оптимальное значение прогнозной функции Тп. После чего выбирается схема формирования и соответствующая декомпозиция, дающие наилучшие прогнозные значения трудоемкости параллельного вычисления.

В третьей главе приведено описание архитектуры и основных функций ППП D-SAT, созданного для реализации параллельной технологии, предложенной во второй главе. ППП D-SAT был использован в решении задач логического криптоанализа ряда генераторов, последовательный логический криптоанализ которых не дал приемлемых результатов.

ППП D-SAT функционирует в РВС под управлением инструментального комплекса Distributed Computing system of Modular Programming (DISCOMP), разработанного в ИДСТУ CO РАН. Библиотека программ ППП D-SAT включает модуль расщепления, модуль SAT-решателя, модуль прогнозирования, модуль сравнения, аналитический модуль и транспортный модуль.

Модуль расщепления используется для декомпозиции исходной КНФ. В данном модуле реализован ряд схем формирования. Основные входные данные модуля расщепления - это файл с исходной КНФ в формате DIMACS, номер y'e{l,...,p} схемы формирования, диапазон значений сij (размерности декомпозиционного множества) и фиксированное значение q, определяющее

число КНФ в произвольной случайной выборке. Обозначим через dj'n и ii;max натуральные числа, определяющие соответственно левую и правую границы интервала, в котором изменяются значения dj. Для каждого значения диапазона

значений dj е {dj'm,...,dj'°*} строится отдельное семейство КНФ. В случае

q < 2J' из декомпозиционного семейства случайным образом выбираются q

КНФ. Если q = 0 или q > 2dj, то выборкой является все рассматриваемое семейство. Результатом декомпозиции является набор файлов, содержащий КНФ, представленные в формате DIMACS. Данный набор описывается в виде параллельного списка. Вычислительное ядро модуля SAT-решателя составляет программа minisat3 версии 2.0. По входному файлу, в котором КНФ представлена в формате DIMACS, модуль SAT-решателя осуществляет поиск выполняющего данную КНФ набора, либо выдает значение NULL в случае отсутствия такового. В выходной файл каждой копии модуля SAT-решателя записывается информация о результатах его работы. Модуль прогнозирования получает на вход файлы с результатами работы модуля SAT-решателя, значение с/ и число г

вычислительных узлов РВС, относительно которого строится прогноз. Модуль строит прогноз оптимального (с точки зрения вычислительных затрат) значения

dj. Данное значение обозначается через dj. Транспортный модуль

осуществляет рассылку КНФ из параллельного списка. Модуль сравнения

получает на вход прогнозные значения d[,...,d'p и выдает значение

d' е {d*,...,d'p} с наилучшим прогнозом, а также соответствующий значению d*

индекс схемы формирования / е {l,...,/>}. Аналитический модуль проверяет найденный выполняющий набор на корректность и сравнивает прогнозируемое время решения с реальным временем.

ППП D-SAT может функционировать в следующих режимах: режим прогнозирования; режим решения SAT-задачи и режим прогнозирования с последующим решением SAT-задачи.

Режим прогнозирования может быть использован для прогнозирования на персональных компьютерах (ПК) трудоемкости параллельного решения SAT-

3 http://minisat.se/MiniSat.html

задач на мощных вычислительных кластерах, доступ к которым ограничен. Если мощность ПК сопоставима с мощностью вычислительного узла кластера, то результаты экспериментов на ПК можно с учетом транспортных расходов экстраполировать на кластер.

С помощью ППП D-SAT был осуществлен успешный параллельный логический криптоанализ генератора Гиффорда, а также суммирующего и порогового генераторов (последовательный логический криптоанализ в отношении этих генераторов оказался малоэффективным). В качестве подтверждения эффективности предлагаемой в работе технологии приведем результаты параллельного логического криптоанализа порогового генератора.

В пороговом генераторе выходные биты zj,ie{\,...,R}, сдвигаемых одновременно (в моменты времени т е N) R регистров сдвига с линейной обратной связью4 (РСЛОС) смешиваются посредством нелинейной булевой функции. В пороговом генераторе для этих целей используется мажоритарная функция.

1 R

>J

А

РСЛОС 1

РСЛОС 2 2 »

■ ■ ■ 4

РСЛОС R

=

R i=1

Рассматривался вариант порогового генератора с 72-битной инициализирующей последовательностью на основе пяти РСЛОС, имеющих следующие порождающие многочлены: (X11 + Х™ +ХЪ + X3 +1); (Хп + X9 + А-8 + X2 + 1); (X15 +Х[4+Хп+Х2+1); (X16+Х14+Х*+Х]+1);

4 Алферов А.П., Зубов А.Ю., Кузьмин A.C., Черемушкин A.B. Основы криптографии. - М.: Гелиос АРВ, 2002. - 480 с.

+ X^ + Xй + X]2 + Xй + Xю + 1). Анализировался фрагмент ключевого потока длиной 150 бит. В следующей таблице приведены результаты параллельного логического криптоанализа порогового генератора рассмотренного выше вида на вычислительном кластере Blackford ИДСТУ СО РАН5 (40 четырехядерных процессоров).

Время решения на одном ядре кластера Прогноз времени решения на кластере Реальное время решения на кластере

> 2 суток 15 - 20 мин. 6-10 мин.

Таблица. Результаты параллельного логического криптоанализа 72-битного порогового генератора (серия тестов).

В заключении сформулированы основные результаты диссертационной работы:

1. Разработана крупноблочная параллельная технология решения 8АТ-задач. Исследованы декомпозиционные представления БАТ-задач. Разработаны и проанализированы различные схемы формирования, ориентированные на структуру БАТ-задач, кодирующих задачи криптоанализа некоторых генераторов ключевого потока.

2. Разработана процедура прогнозирования трудоемкости параллельного решения БАТ-задач. Получена оценка сложности процедуры прогнозирования времени параллельного решения БАТ-задач.

3. Разработан ППП Ь-БАТ для практической реализации предложенной параллельной технологии решения БАТ-задач. С помощью ППП Б-БАТ решены БАТ-задачи, кодирующие логический криптоанализ генератора Гиффорда, а также суммирующего и порогового генераторов.

5 http://www.mvs.icc.ru

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Заикин О.С., Семенов A.A. Технология крупноблочного параллелизма в SAT-задачах // Проблемы управления. - 2008. - № 1. - С. 4350.

2. Семенов A.A., Заикин О.С., Беспалов Д.В., Ушаков A.A. SAT-подход в криптоанализе некоторых систем поточного шифрования // Вычислительные технологии. - 2008. Т. 13, № 6. - С. 133-149.

3. Заикин О.С. Об одной эвристике в задаче поиска выполняющего набора выполнимой КНФ // Тезисы докладов VI школы-семинара молодых ученых «ММИТ». - Иркутск: ИДСТУ СО РАН, 2008. - С. 19.

4. Семенов A.A., Заикин О.С. Об одном подходе к поиску выполняющих наборов одновыполнимых КНФ // Материалы II Всероссийской конференции с международным участием «Инфокоммуникационные и вычислительные технологии и системы» (ИКВТС-06). - Улан-Удэ: БГУ, 2006. - Т. 2. - С. 122-126.

5. Заикин О.С. Параллельный подход к логическому криптоанализу некоторых генераторов двоичных последовательностей // Материалы конференции «Ляпуновские чтения». - Иркутск: ИДСТУ СО РАН, 2006. - С. 16.

6. Заикин О.С. Применение вычислительных кластеров в криптоанализе генераторов двоичных последовательностей. // Избранные материалы Шестой школы-семинара «Распределенные и Кластерные вычисления». Красноярск: ИВМ СО РАН, 2007. - С. 31-36.

7. Заикин О.С., Сидоров И.А. Технология крупноблочного распараллеливания в криптоанализе некоторых генераторов двоичных последовательностей // Труды международной научной конференции ПАВТ'07. Челябинск: ЮУрГУ, 2007. - Т. 1. - С. 158-169.

8. Семенов A.A., Заикин О.С. Технология крупноблочного параллелизма в SAT-задачах // Материалы XV международной конференции по вычислительной механике и современным прикладным программным системам (ВМСППС '2007).-С. 230-231.

9. Заикин О.С., Семенов A.A., Сидоров И.А., Феоктистов А.Г. Параллельная технология решения SAT-задач с применением пакета прикладных программ D-SAT. // Вестник ТГУ. Приложение. - 2007. -№ 23. - С. 83-95.

10. Заикин О.С. Реализация технологии решения SAT-задач с применением пакета прикладных программ D-SAT // Тезисы докладов IX школы-семинара молодых ученых «ММИТ». Иркутск: ИДСТУ СОРАН, 2007. - С. 73-76.

11. Заикин О.С. Использование пакета прикладных программ D-SAT для решения SAT-задач // Материалы конференции «Ляпуновские чтения». Иркутск: ИДСТУ СО РАН, 2007. - С. 9.

12. Семенов A.A., Заикин О.С. Неполные алгоритмы в крупноблочном траллелизме комбинаторных задач // Труды международной научной онференции ПАВТ'08. Санкт-Петербург, 2008. - С. 232-244.

13. Заикин О.С. Пакет прикладных программ Distributed-SAT: Свидетельство об официальной регистрации программы для ЭВМ № 008610423. - М.: Федеральная служба по интеллектуальной собственности, атентам и товарным знакам, 2008.

14. Семенов A.A., Заикин О.С. Неполные алгоритмы в крупноблочном траллелизме комбинаторных задач // Вычислительные методы и фограммнрование. - 2008. - Том 9, № 1. - С. 112-122.

15. Заикин О.С. Декомпозиционные представления данных в руиноблочном параллелизме SAT-задач // Прикладные алгоритмы в дискретном напизе. Иркутск: ИГУ, 2008. - Серия: Дискретный анализ и информатика, вып. . - С. 49-69.

16. Семенов A.A., Заикин О.С., Отпущенников И.В., Буров П.С. некоторых особенностях задач обращения дискретных функций // Труды XIV

айкальской Международной школы-семинара «Методы оптимизации и их риложения». - Иркутск: ИСЭМ СО РАН, 2008. Т. 1.-С. 498-505.

17. Семенов A.A., Заикин О.С., Беспалов Д.В., Хмельнов А.Г., Буров П.С. нализ некоторых криптографических примитивов на вычислительных ластерах // Прикладная дискретная математика. 2008. - № 2. - С. 120-130.

18. Семенов A.A., Заикин О.С., Беспалов Д.В., Хмельнов А.Г., Буров П.С. ешение задач обращения дискретных функций на многопроцессорных ычислительных системах // Труды Четвертой Международной конференции Параллельные вычисления и задачи управления» РАСО'2008. М.: Институт роблем управления им. В.А. Трапезникова РАН, 2008. - С. 152-176.

Редакционно-издательский отдел Института динамики систем и теории управления СО РАН 664033, Иркутск, ул. Лермонтова, д. 143 Подписано к печати 10.12.2008 Формат бумаги 60x84 1/16, объем 1,2 п.л. Заказ 12. Тираж 100 экз.

Отпечатано в ИДСТУ СО РАН

Введение.

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

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

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

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

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

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

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

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

2.4. Схемы формирования декомпозиционных множеств.

Глава 3. Пакет прикладных программ Б-БАТ и вычислительные эксперименты.

3.1. Описание пакета прикладных программ Б-ЭАТ.

3.1.1. Библиотека программ пакета Б-8АТ.

3.1.2. Режимы работы пакета В-8АТ.

3.1.3. Дополнительные аспекты пакета Б-8АТ.

3.2. Параллельный логический криптоанализ некоторых генераторов ключевого потока.

3.2.1. Особенности пропозиционального кодирования генераторов ключевого потока.

3.2.1. Криптоанализ генератора Гиффорда.

3.2.2. Криптоанализ суммирующего генератора.

3.2.3. Криптоанализ порогового генератора.

3.2.4. Прогнозирование трудоемкости параллельного логического криптоанализа генератора А5/1.

Актуальность работы

Многие значимые в практическом отношении проблемы, связанные с управлением и обработкой информации в дискретных системах, допускают эффективные сводимости к задачам поиска решений логических уравнений. Сказанное касается проблем синтеза и верификации в микроэлектронике, целого ряда вопросов теоретического программирования, задач обращения дискретных функций, задач управления коммуникационными протоколами и многих других. Один из наиболее важных классов логических уравнений образован уравнениями вида «КНФ =1» (КНФ - конъюнктивная нормальная форма). Задачи поиска решений данного класса уравнений относятся к так называемым «SAT-задачам». Для решения SAT-задач используются специальные программные комплексы, называемые SAT-решателями. В построении SAT-решателей в последние годы отмечен реальный прогресс.

Высокая вычислительная сложность SAT-задач аргументирует использование для их решения параллельных вычислений. С этой позиции SAT-задачи могут исследоваться по двум направлениям.

Первое направление основывается на концепции мелкозернистого параллелизма. В этом случае распараллеливание осуществляется на уровне базового алгоритма SAT-решателя (SAT-решатели с параллельной вычислительной архитектурой). Однако современные SAT-решатели являются довольно сложными в структурном смысле программами, в связи с чем реализация данного подхода трудна в техническом отношении. Кроме этого, мелкозернистый параллелизм зачастую характеризуется невысокой масштабируемостью.

В основе второго направления лежит концепция крупноблочного параллелизма. В этом случае осуществляется декомпозиция исходной SAT-задачи на семейство подзадач, каждая из которых обрабатывается SATрешателем на отдельном вычислительном узле параллельной вычислительной системы. При этом параллельная вычислительная система свободна от ряда ограничений, присущих мелкозернистому параллелизму. Кроме этого, крупноблочный подход, как правило, характеризуется высокой масштабируемостью. Крупноблочный параллелизм предпочтителен в решении SAT-задач, в которых размерность пространства полного перебора существенно меньше числа булевых переменных, фигурирующих в КНФ. Речь идет, прежде всего, о SAT-задачах, к которым сводятся задачи обращения дискретных функций из класса, имеющего пересечения с многочисленными областями кибернетики.

Сказанное означает, что проблема создания эффективных технологий решения SAT-задач посредством их крупноблочного распараллеливания является актуальной.

Цель работы и задачи исследования

Целью диссертационной работы является разработка и практическая реализация технологии крупноблочного распараллеливания SAT-задач.

Для достижения указанной цели ставятся и решаются следующие основные задачи.

1. Разработка и исследование различных стратегий построения декомпозиционных представлений SAT-задач.

2. Разработка и алгоритмическая реализация процедуры прогнозирования трудоемкости параллельного решения SAT-задач.

3. Программная реализация технологии крупноблочного распараллеливания SAT-задач в форме пакета прикладных программ (111111).

4. Решение с помощью разработанного 111111 SAT-задач, кодирующих задачи обращения ряда дискретных функций, используемых в криптографии.

Методы исследования

Теоретические исследования используют аппарат теории множеств, дискретной математики, теории вычислительной сложности, параллельных вычислений, а экспериментальные - инструментальные и программные средства решения задач в параллельных вычислительных системах.

Научная новизна

Новыми являются все основные результаты, полученные в диссертации, в том числе:

- общая схема крупноблочного распараллеливания SAT-задач;

- процедура прогнозирования трудоемкости параллельного решения SAT-задач;

- оценка сложности процедуры прогнозирования трудоемкости параллельного решения SAT-задач;

- разработка ППП для реализации параллельной технологии решения SAT-задач;

- параллельное решение с помощью разработанного ППП вычислительно сложных SAT-задач, кодирующих задачи обращения некоторых дискретных функций, используемых в криптографии.

При решении поставленных задач были получены перечисленные ниже вспомогательные результаты, представляющие самостоятельный интерес. Введено понятие декомпозиционного множества; введено понятие схемы формирования семейств декомпозиционных множеств (далее «схема формирования»); введена классификация схем формирований; разработаны схемы формирования, ориентированные на структуру SAT-задач, кодирующих задачи обращения некоторых дискретных функций; реализована процедура оптимизированной рассылки SAT-задач, снижающая транспортные расходы в параллельных вычислительных системах.

Теоретическая и практическая значимость работы

Теоретическая значимость работы аргументируется возможностью прямого переноса ее базовых концепций на задачи дискретной оптимизации с двоичными данными. Разработанные в диссертации методы и алгоритмы могут применяться для решения широкого класса практически важных задач, допускающих эффективную сводимость к SAT-задачам.

Достоверность результатов

Достоверность полученных в работе теоретических результатов обеспечивается строгостью производимых математических построений. Корректность и эффективность практической реализации подтверждается результатами вычислительных экспериментов.

Основные результаты, выносимые на защиту

1. Параллельная технология решения SAT-задач, включающая общую схему крупноблочного распараллеливания SAT-задач.

2. Разработка и анализ различных схем формирования декомпозиционных представлений SAT-задач.

3. Процедура прогнозирования трудоемкости параллельного решения SAT-задач; оценка сложности данной процедуры.

4. Разработка 111111 для практической реализации предложенной параллельной технологии решения SAT-задач.

5. Параллельное решение с помощью разработанного 111111 вычислительно сложных SAT-задач, кодирующих задачи обращения некоторых дискретных функций, используемых в криптографии.

Работа состоит из введения, 3-х глав, заключения и списка литературы.

В первой главе описывается SAT-подход к решению задач обращения дискретных функций. Приведен обзор основных компонентов архитектуры современных SAT-решателей. Описана концепция логического криптоанализа.

В разделе 1.1 рассматривается специальный класс з, образованный всеми всюду определенными алгоритмически вычислимыми (за полиномиальное от длины входа время) семействами дискретных функций. Задача обращения дискретной функции семейства 3 ставится следующим образом: по известному образу найти хотя бы один прообраз. Проблемы обращения функций произвольного семейства из класса 3 допускают эффективную сводимость к проблемам поиска решений логических уравнений вида «КНФ=1», где КНФ - это конъюнктивная нормальная форма над некоторым множеством булевых переменных. Задачи поиска решений таких уравнений называются SAT-задачами.

В разделе 1.2 рассмотрены основные компоненты архитектуры современных эффективных SAT-решателей (программных комплексов, решающих SAT-задачи), основанных на алгоритме DPLL. Приведен обзор следующих базовых технологий, используемых в такого рода SAT-решателях: бэктрекинг, нехронологический бэктрекинг, правило единичного дизъюнкта, ВСР-стратегия, процедура «Clause Learning», процедуры чистки базы ограничений, рестарты.

В разделе 1.3 описывается концепция логического криптоанализа (криптоанализ, рассматриваемый как SAT-задача). В отношении генераторов ключевого потока приводится постановка логического криптоанализа как задачи обращения дискретных функция из класса 3.

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

В разделе 2.1 кратко охарактеризованы особенности мелкозернистого и крупноблочного подходов к параллельному решению 8АТ-задач.

В разделе 2.2 описана методика крупноблочного распараллеливания ЭАТ-задач. Общая идея данной методики состоит в следующем.

Рассматривается произвольная КНФ (называемая далее исходной) над множеством булевых переменных X. Декомпозиционным множеством называется некоторое подмножество X' множества X. Декомпозиционному множеству X' ставится в соответствие множество у(х')={у1,.,ук}, состоящее из к = 2л различных двоичных векторов, каждый из которых является вектором значений переменных из X1. Декомпозиционным семейством называется множество КНФ, полученных подстановками в исходную КНФ векторов из Всякому набору, выполняющему исходную КНФ, соответствует набор, выполняющий некоторую КНФ из декомпозиционного семейства. Наоборот, произвольному набору, выполняющему некоторую КНФ из декомпозиционного семейства, соответствует единственный набор, выполняющий исходную КНФ. Таким образом, БАТ-задача относительно исходной КНФ сводится к решению БАТ-задач для КНФ из декомпозиционного семейства.

В разделе 2.3 предложена процедура прогнозирования трудоемкости параллельного решения 8АТ-задач при их крупноблочном распараллеливании.

Предположим, что зафиксировано некоторое декомпозиционное множество X'. Представляет интерес «улучшение» X, то есть построение такого подмножества X', использование которого в качестве декомпозиционного множества делают декомпозицию более эффективной, чем на основе X'.

Предлагается специальная процедура статистического прогнозирования, предназначенная для «улучшения» декомпозиционного множества. Представление о трудоемкости соответствующего параллельного вычисления можно составить на основе знания среднего времени решения SAT-задач для серии КНФ, выбранных случайным образом из декомпозиционного множества. Введена специальная прогнозная функция и задача выбора оптимального (по прогнозу) декомпозиционного множества решается через задачу оптимизации данной функции.

В разделе 2.4 предлагается методика построения декомпозиционных множеств. Основой данной методики является понятие схемы формирования декомпозиционного множества (далее «схема формирования»). Схема формирования - это алгоритм построения декомпозиционных множеств заданной мощности. Здесь же предлагается совмещение технологии статистического прогнозирования с использованием различных схем формирования. При этом каждой схеме формирования ставится в соответствие прогноз трудоемкости параллельного вычисления, после чего выбирается схема формирования и соответствующая декомпозиция, дающие наилучшие прогнозные значения.

В третьей главе приведено описание пакета прикладных программ (111111) D-SAT1 (созданного для реализации параллельной технологии, предложенной во второй главе), а также результаты вычислительных экспериментов.

В разделе 3.1 описаны архитектура и основные функции 111111D-SAT.

Ill 111 D-SAT функционирует в РВС под управлением инструментального комплекса Distributed Computing system of Modular Programming (DISCOMP2). Библиотека программ 111111 D-SAT включает модуль расщепления, модуль SAT-решателя, модуль прогнозирования, модуль сравнения, аналитический модуль и транспортный модуль.

1 Заикин О.С. Пакет прикладных программ 01зйчЬШес1-8АТ: Свидетельство об официальной регистрации программы для ЭВМ № 2008610423. — М.: Федеральная служба по интеллектуальной собственности, патентам и товарным знакам, 2008.

2 Разработчик Сидоров И.А., ИДСТУ СО РАН

В разделе 3.2 на серии численных экспериментов продемонстрировано успешное использование ППП D-SAT в решении задач логического криптоанализа ряда генераторов, последовательный логический криптоанализ которых не дал приемлемых результатов. Так, с помощью ППП D-SAT был осуществлен успешный параллельной логический криптоанализ генератора Гиффорда, а также суммирующего и порогового генераторов.

Внедрение результатов исследований

Результаты диссертации внедрены:

1) в разработку технологии крупноблочного распараллеливания SAT-задач в рамках следующих грантов РФФИ: № 04-07-90358 (2006 г.), № 07-01-00400-а (2007-2008 гг.), а также грантов поддержки ведущих научных школ: НШ-9508.2006.1 (2006 г.), НШ-1676.2008.1 (2008 г.);

2) в создание lililí Distributed-SAT (D-SAT), предназначенного для параллельного решения SAT-задач: свидетельство № 2008610423 об официальной регистрации программы для ЭВМ, выданное Федеральной службой по интеллектуальной собственности, патентам и товарным знакам (2008 г.);

3) в учебный процесс (разработка курсовых и дипломных работ) Института математики, экономики и информатики Иркутского государственного университета (ИМЭИ ИГУ).

Копии документов о внедрении приведены в приложении 2.

Апробация работы

Результаты диссертации докладывались и обсуждались на 1-ой и 2-ой Международных научных конференциях «Параллельные вычислительные технологии (ПАВТ)» (Челябинск, 2007; Санкт-Петербург, 2008), на 4-ой Международной конференции «Параллельные вычисления и задачи управления (РАСО'2008)» (Москва, 2008), на XV Международной конференции «Вычислительная механика и современные прикладные программные системы (ВМСППС'2007)» (Алушта, 2007), на XIV Байкальской международной школе-семинаре «Методы оптимизации и их приложения» (Северобайкальск, 2008 г.) на VI и VII Сибирских научных школах-семинарах с международным участием «Компьютерная безопасность и криптография» (Горно-Алтайск, 2007; Красноярск, 2008), на II Всероссийской конференции с международным участием «Инфокоммуникационные и вычислительные технологии и системы (ИКВТС'2006)» (Улан-Удэ, 2006), на 6-ой школе-семинаре «Распределенные и кластерные вычисления» (Красноярск, 2006), на научных конференциях «Ляпуновские чтения» (Иркутск, 2006; 2007), на VI и IX школах-семинарах молодых ученых «ММИТ» (Иркутск, 2005; 2007); на научных семинарах Института динамики систем и теории управления СО РАН, а также на научном семинаре кафедры защиты информации и криптографии Томского государственного университета (2008 г.).

Структура работы и личный вклад автора

Диссертация состоит из введения, трех глав, заключения и списка литературы, насчитывающего 105 наименований, изложена на 116 страницах, содержит 14 иллюстраций и 7 таблиц. Первая глава является обзорной, в ней отражены в основном известные результаты. Часть результатов второй главы (введение прогнозных функций, оценка сложности процедур прогнозирования времени параллельного решения 8АТ-задач) получены в неделимом соавторстве с научным руководителем. Все остальные результаты, представленные в диссертации, получены автором лично.

Заключение

Перечислим основные результаты диссертационной работы.

1. Разработана параллельная технология решения SAT-задач. Исследованы декомпозиционные представления SAT-задач. Разработаны и проанализированы различные схемы формирования, ориентированные на структуру SAT-задач, кодирующих задачи криптоанализа некоторых генераторов ключевого потока.

2. Разработана процедура прогнозирования трудоемкости параллельного решения SAT-задач. Получена оценка сложности процедуры прогнозирования трудоемкости параллельного решения SAT-задач.

3. Разработан lililí D-SAT для практической реализации предложенной параллельной технологии решения SAT-задач. С помощью lililí D-SAT решены SAT-задачи, кодирующие логический криптоанализ генератора Гиффорда, а также суммирующего и порогового генераторов.

Дополнительно отметим, что ускорение, достигаемое при параллельном решении SAT-задач, кодирующих логический криптоанализ порогового генератора, существенно превышало число вычислительных единиц задействованной РВС (в сравнении с временем последовательного криптоанализа на одной вычислительной единице). Данный факт может рассматриваться как дополнительный аргумент эффективности предлагаемой в диссертации технологии.

1. Яблонский С.В. Введение в дискретную математику. — М.: Наука, 1986. -384 с.

2. Мендельсон Э. Введение в математическую логику. М.: Наука, 1971.- 320 с.

3. Катленд Н. Вычислимость. Введение в теорию рекурсивных функций. -М.: Мир, 1983.-256 с.

4. Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. М.: Мир, 1982. - 416 с.

5. Семенов А.А. О сложности обращения дискретных функций из одного класса // Дискретный анализ и исследование операций. 2004. - Т. 11.- № 4. — С. 44-55.

6. Buchberger В. Groebner bases: an algorithmic method in polynomial ideal theory, in Multidimensional System Theory, ed. by Bose N.K., D. Reidel Publishing Company, Dordrecht. P. 184-232.

7. Кокс Д., Литтл Дж., О'Ши Д. Идеалы, многообразия и алгоритмы. М.: Мир, 2000. - 687 с.

8. Агибалов Г.П. Логические уравнения в криптоанализе генераторов ключевого потока // Вестник Томского гос. ун-та. — Приложение. —2003.-№ 6.-С. 31-41.

9. Тимошевская Н.Е. Параллельные вычисления в решении систем логических уравнений методом линеаризации // Материалы XV международной школы-семинара «Синтез и сложность управляющих систем». Новосибирск: Институт математики, 2004. - С. 97 - 102.

10. Тимошевская Н.Е. Задача о кратчайшем линеаризационном множестве // Вестник Томского госуниверситета. — Приложение. -2005.-№ 14.-С. 79-83.

11. Тимошевская Н.Е. О линеаризационно эквивалентных покрытиях // Вестник Томского госуниверситета. Приложение. - 2005. - № 14 -С. 84-91.

12. Bryant R.E. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35(8), 1986. P. 677-691.

13. Meinel Ch., Theobald T. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications. Springer-Verlag, Berlin, Heidelberg, New York, 1998.

14. Семенов А.А., Беспалов Д.В. Технологии решения многомерных задач логического поиска // Вестник Томского гос. ун-та. — Приложение. -2005. -№ 14.-С. 61-73.

15. Семенов А.А. Трансляция алгоритмов вычисления дискретных функций в выражения пропозициональной логики. Прикладные алгоритмы в дискретном анализе. Серия: Дискретный анализ и информатика. Иркутск: Изд-во ИГУ, 2008. Вып. 2. С. 70-98.

16. М. Davis and Н. Putnam. A computing procedure for quantification theory.

17. J. of ACM, 7:201-215, 1960.

18. Robinson J.A. A machine-oriented logic based on the resolution principle // J. ACM, v.12, no. 1 pp. 23-41, 1965.

19. Чень Ч., Ли P. Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983. — 360 с.

20. Семенов А.А. Логико-эвристический подход в криптоанализе генераторов двоичных последовательностей // Труды международной научной конференции ПАВТ'07. Челябинск: ЮУрГУ, 2007. Т. 1, С. 170-180.

21. Цейтин Г.С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР, 1968, Т.8. - С. 234259.

22. J.F. Groote and H. Zantema. Resolution and binary decision diagrams cannot simulate each other polynomially. Journal of Discrete Applied Mathematics, volume 130, issue 2, pages 157-171, 2003.

23. N. Een, N. Sorensson Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation. 2006. N2. p. 1-25.

24. Gu J., Purdom P., Franco J., Wah B.W. Algorithms for the satisfiability problem. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2000.

25. Тей А., Грибомон П., Луи Ж. и др. Логический подход к искусственному интеллекту. М.: Мир, 1991. — 429 с.

26. Пападимитриу X., Стайглиц К. Комбинаторная оптимизация.

27. Алгоритмы и сложность. М.: Мир, 1985. - 510 с.

28. M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Communication of the ACM, 5: 394-397, 1962.

29. Marqeus-Silva J. P. Sakallah K.A. GRASP: A search algorithm for propositional satisfiability. IEEE Trans, on Computers, vol. 48, No. 5, May, 1999, pp. 506-521.

30. SatLive http://www.satlive.org.

31. Zhang L., Madigan C., Moskewicz M., Malik S. Efficient conflict driven learning in a Boolean satisfiability solver. In Proc. of the International Conference on Computer Aided Design (ICCAD), San Jose, California, 11, 2001.

32. Заикин O.C. Об одной эвристике в задаче поиска выполняющего набора выполнимой КНФ // Тезисы докладов VI школы-семинара молодых ученых «ММИТ». Иркутск: ИДСТУ СО РАН, 2005. -С. 19.

33. Moskewicz M., Madigan С., Zhao Y., Zhang L., Malik S. Chaff: Engineering an Efficient SAT Solver. Proc. Design Automation Conference (DAC 2001), July, 2001.

34. Семенов A.A., Заикин O.C. Неполные алгоритмы в крупноблочном параллелизме комбинаторных задач // Вычислительные методы и программирование. 2008. - Том 9. - № 1. - С. 112-122.

35. Zhang H., SATO: An efficient propositional prover. In proc. of Int. conf. on Automated deduction, pp. 272-275, July, 1997.

36. Inès Lynce and Joâo P. Marques-Silva, Efficient data structures forbacktrack search SAT solvers, 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT'02), May 2002.

37. Miroslav N. Velev, Randal E. Bryant: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. 35(2): 73-106 (2003).

38. Закревский А.Д., Поттосин Ю.В., Черемисинова Л.Д. Логические основы проектирования дискретных устройств. М.: ФИЗМАТ ЛИТ, 2007. - 590 с.

39. Колмероэ А., Кануи А., ван Канегем М. Пролог теоретические основы и современное развитие. — В сб. Логическое программирование. -М.: Мир, 1988. - С. 27-133.

40. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. -М.: МЦНМО, 2002.

41. Н.О. Гаранина, Н.В. Шилов. Верификация комбинированных логик знаний, действий и времени в моделях // Системная информатика. -2005.-Вып. 10.-С. 114-173.

42. Amman P., Ritchey R. Using Model Checking to Analyze Network Vulnerabilities // Proc. Of the 2000 IEEE Symposium on Security and Privacy, 2000. P. 156-165.

43. Sheyer O., Jha S., Wing J., et al. Automated Generation and Analysis of Attack Graphs // 2002 IEEE Symposium on Security and Privacy. 2002.

44. Заикин O.C., Семенов A.A. Технология крупноблочного параллелизма в SAT-задачах // Проблемы управления. 2008. - № 1. - С. 43-50.

45. Massacci F., Marraro L. Logical Cryptoanalysis as a SAT Problem: the Encoding of the Data Encryption Standard. Preprint. Dipartimento di Imformatica e Sistemistica, Universita di Roma "La Sapienza", 1999.

46. Агибалов Г.П. Избранные теоремы начального курса криптографии: Учебное пособие. — Томск: НТЛ, 2005. 116 с.

47. Menezes A., Van Oorschot P., Vanstone S. Handbook of Applied

48. Cryptography. CRC Press, 1996. - 657 с.

49. Месси Дж.Л. Введение в современную криптологию // ТИИЭР. 1988. -Т. 76.-№5.-С 24-42.

50. Арто Саломаа. Криптография с открытым ключом. М., 1995.

51. Шеннон К. Э. Теория связи в секретных системах // Работы по теории информации и кибернетике. -М.: ИЛ, 1963. С. 333-369.

52. Шеннон К. Э. Математическая теория связи // Работы по теории информации и кибернетике. М.: ИЛ, 1963. - С. 333-369.

53. Diffie W., Hellman М. Е., New Directions in Cryptography // IEEE Transactions on Information Theory. 1976. - V. IT-22.N.6. -P.644-654.

54. Семенов A.A. Разрешимость симметричных шифров. // Вестник Томского государственного университета. Томск. -Приложение. -2003.-№6.-С. 65-70.

55. Буранов Е.В. Программная трансляция процедур логического криптоанализа симметричных шифров // Вестник Томского гос. ун-та. Приложение. - 2004. - № 9 (1). - С. 60-65.

56. Поточные шифры. Результаты зарубежной открытой криптологии. -М.:Мир, 1997.-389 с.

57. Коваленко В.Н., Корягин Д.А. Вычислительная инфраструктура будущего // Открытые системы. 1999. - № 11-12. - С. 45-53.

58. Воеводин В.В., Воеводин Вл.В. Параллельные вычисления. СПб.: БХВ-Петербург, 2002. - 608 с.

59. Воеводин Вл.В., Филамофитский М.П. Суперкомпьютер на выходные // Открытые системы. 2003. - № 5. - С. 48-56.

60. Бандман О.Л. Мелкозернистый параллелизм в вычислительной математике // Программирование. — 2001. — № 4. — С. 5-20.

61. Бандман О.Л. Методы параллельного микропрограммирования. -Новосибирск: Наука, 1981.

62. Бандман О.Л. Клеточно-автоматное моделирование пространственнойдинамики // Системы информатики. Новосибирск: СО РАН, 2000. -Вып. 10.-С. 59-113.

63. Fran Berman Grid Computing: Making The Global Infrastructure a Reality.

64. Фаддеев Д.К., Фаддеева B.H. Параллельные вычисления линейной алгебры // Кибернетика, 1977. № 6. - С. 28-40.

65. Тимошевская Н.Е. Параллельные методы обхода дерева // Математическое моделирование. 2004. - Том 16. — № 1. — С. 105114.

66. М. Böhm and Е. Speckenmeyer. A fast parallel SAT-solver efficient workload balancing. Annals of Mathematics and Artificial Intelligence, Volume 17, №2, 1996. - P. 381-400.

67. SAT-Race 2008: http://www-sr.infonnatik.uni-tuebingen.de/sat-race-2008/.

68. Заикин O.C., Сидоров H.A. Технология крупноблочного распараллеливания в криптоанализе некоторых генераторов двоичных последовательностей // Труды международной научной конференции ПАВТ'07. Челябинск: ЮУрГУ, 2007. Т. 1. - С. 158-169.

69. Заикин О.С., Семенов A.A., Сидоров H.A., Феоктистов А.Г. Параллельная технология решения SAT-задач с применением пакета прикладных программ D-SAT. // Вестник ТГУ. Приложение. - 2007. -№ 23. - С. 83-95.

70. Опарин Г.А., Богданова В.Г., Сидоров H.A. Интеллектуальный решатель задач в булевых ограничениях в распределенной вычислительной среде // Информационные и математические технологии в науке и управлении. Иркутск: ИСЭМ РАН, 2007. - С. 32-40.

71. Семенов A.A., Заикин О.С. Технология крупноблочного параллелизма в SAT-задачах // Материалы XV международной конференции по вычислительной механике и современным прикладным программнымсистемам (ВМСППС '2007). С. 230-231.

72. Кормен, Т.Х., Лейзерсон, Ч.И., Ривест P.JL, Штайн К. Алгоритмы: построение и анализ, 2-е издание. : Пер. с англ. М. : Издательский дом «Вильяме», 2005. - 1296 с.

73. Заикин О.С. Декомпозиционные представления данных в крупноблочном параллелизме SAT-задач // Прикладные алгоритмы в дискретном анализе. Иркутск: ИГУ, 2008. — Серия: Дискретный анализ и информатика, вып. 2. С. 49-69.

74. J.W. Freeman. Improvements to Propositional Satisfiability. PhD thesis, University of Pennsylvania, Philadelphia(PA), May 1995.

75. R.G Jeroslaw and J. Wang. Solving propositional satisfiability problems. Annals of mathematics and Artificial Intelligence, 1:167-187, 1990.

76. Семенов A.A., Отпущенников И.В. Об алгоритмах обращения дискретных функций из одного класса. // Прикладные алгоритмы в дискретном анализе. Серия: Дискретный анализ и информатика. Иркутск: Изд-во ИГУ, 2008. Вып. 2. - С. 127-156.

77. Заикин О.С. Пакет прикладных программ Distributed-SAT: Свидетельство об официальной регистрации программы для ЭВМ № 2008610423. — М.: Федеральная служба по интеллектуальной собственности, патентам и товарным знакам, 2008.

78. Заикин О.С. Реализация технологии решения SAT-задач с применением пакета прикладных программ D-SAT // Тезисы докладов IX школы-семинара молодых ученых «ММИТ». Иркутск: ИДСТУ СОРАН, 2007.-С. 73-76.

79. Заикин О.С. Использование пакета прикладных программ D-SAT для решения SAT-задач // Материалы конференции «Ляпуновские чтения». Иркутск: ИДСТУ СО РАН, 2007. С. 9.

80. Тыугу Э.Х. Концептуальное программирование. М.: Наука, 1984. -256 с.

81. Горбунов-Посадов M.M., Корягин Д.А., Мартынюк B.B. Системное обеспечение пакетов прикладных программ. — М.: Наука, 1990. 208 с.

82. Феоктистов А.Г., Сидоров H.A. Языковые средства описания распределенных вычислений в инструментальном комплексе DISCOMP // Труды международной научной конференции ПАВТ'08. Санкт-Петербург, 2008. - С. 488-493.

83. Сидоров И.А., Тятюшкин А.И., Феоктистов А.Г. Распределенная информационно-вычислительная среда модульного программирования // Параллельные вычисления и задачи управления: Труды III Межд. конф. РАСО'2006. Москва: ИЛУ РАН, 2006.

84. Стандарт POSIX (Portable Operating System Interface for UNIX) http://standards.ieee.org/regauth/posix/.

85. Олейников А.Я. Методика тестирования на соответствие стандартам, обеспечивающим переносимость прикладных программ (POSIX). — Москва, 1999.-31 с.

86. Формат DIMACS http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html.

87. Фергюссон Нильс, Шнайер Брюс. Практическая криптография. : Перевод с англ. М. : Издательский дом «Вильяме», 2005. - 424 с.

88. MiniSat http://minisat.se/MiniSat.html.

89. Zchaff http://www.princeton.edu/~chaff/zchaff.html.

90. Семенов A.A., Заикин О.С., Беспалов Д.В., Хмельнов А.Г., Буров П.С. Анализ некоторых криптографических примитивов на вычислительных кластерах // Прикладная дискретная математика. -2008.-№2.-С. 120-130.

91. Семенов A.A., Ушаков A.A., Буранов Е.В. Эвристический поиск в криптоанализе генераторов двоичных последовательностей // Вестник Томского гос. ун-та. Приложение. - 2006. — № 17. — С. 127-133.

92. Семенов A.A., Заикин О.С., Беспалов Д.В., Ушаков A.A. SAT-подход в криптоанализе некоторых систем поточногошифрования // Вычислительные технологии. — 2008. Т. 13. - № 6. -С. 134-150.

93. Заикин О.С. Применение вычислительных кластеров в криптоанализе генераторов двоичных последовательностей // Избранные материалы Шестой школы-семинара «Распределенные и кластерные вычисления». Красноярск: ИВМ СО РАН, 2007. - С. 31-36.

94. Заикин О.С. Параллельный подход к логическому криптоанализу некоторых генераторов двоичных последовательностей // Материалы конференции «Ляпуновские чтения»: ИДСТУ СО РАН, 2006. С. 16.

95. Суперкомпьютерный центр ИДСТУ СО РАН http://www.mvsлcc.ru.

96. D.K. Gifford, J.M. Lucassen and S.T. Berlin. The Application of Digital Broadcast Communication to Large Scale Information Systems. IEEE Journal on Selected Areas in Communications, v 3, n 3, May 1985. P. 457-467.

97. T.R. Cain and A.T. Sherman. How to break Gifford's Cipher. CRYPTOLOGIA, vol. XXI, 1997, №. 3. P. 237-286.

98. Rueppel R.A., Correlation immunity and the summation combiner. In Lecture Notes in Computer Science 218; Advances in Cryptology: Proc. Crypto'85, H. C. Williams Ed., Santa Barbara, CA, Aug. 18-22, 1985, P. 260-272. Berlin: Springer-Verlag, 1986.

99. Bruer J.O. On pseudo random sequences as crypto generators // In Proc. Int. Zurich Seminar on Digital Communication. —Switzerland, 1984.

100. A. Biryukov, A. Shamir, D. Wagner Real Time Cryptanalysis of A5/1 ona PC. Fast Software Encryption Workshop 2000, April 10-12, 2000, New-York City.

101. Научно-исследовательский вычислительный центр МГУ имени М.В.Ломоносова http://parallel.ru/cluster/.

102. Список суперкомпьютеров топ-50 http://supercomputers.ru/.