Параллельная технология решения SAT-задач и ее реализация в виде пакета прикладных программ тема диссертации и автореферата по ВАК РФ 05.13.01, кандидат технических наук Заикин, Олег Сергеевич

• Заикин, Олег Сергеевич
• кандидат технических наук
• 2008

Оглавление диссертации кандидат технических наук Заикин, Олег Сергеевич

Введение.

Глава 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.

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

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

Многие значимые в практическом отношении проблемы, связанные с управлением и обработкой информации в дискретных системах, допускают эффективные сводимости к задачам поиска решений логических уравнений. Сказанное касается проблем синтеза и верификации в микроэлектронике, целого ряда вопросов теоретического программирования, задач обращения дискретных функций, задач управления коммуникационными протоколами и многих других. Один из наиболее важных классов логических уравнений образован уравнениями вида «КНФ =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-задач, кодирующих логический криптоанализ порогового генератора, существенно превышало число вычислительных единиц задействованной РВС (в сравнении с временем последовательного криптоанализа на одной вычислительной единице). Данный факт может рассматриваться как дополнительный аргумент эффективности предлагаемой в диссертации технологии.

Список литературы диссертационного исследования кандидат технических наук Заикин, Олег Сергеевич, 2008 год

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/.