автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Методы и средства преобразования процедурных описаний дискретных функций в булевы уравнения



ОТПУЩЕННИКОВ ИЛЬЯ ВЛАДИМИРОВИЧ

МЕТОДЫ И СРЕДСТВА ПРЕОБРАЗОВАНИЯ ПРОЦЕДУРНЫХ ОПИСАНИЙ ДИСКРЕТНЫХ ФУНКЦИЙ В БУЛЕВЫ УРАВНЕНИЯ

05.13.11—Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

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

2 6 МАЙ 2011

Иркутск - 2011

4848258

Работа выполнена в Учреждении Российской академии наук Институте динамики систем и теории управления Сибирского отделения РАН (ИДСТУ СО РАН).

Научный руководитель:

кандидат технических наук, доцент

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

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

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

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

кандидат технических наук, доцент

Тренькаев Вадим Николаевич

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

Институт систем информатики им. А. П. Ершова СО РАН (г. Новосибирск)

Защита состоится 14 июня 2011 г. в 15:00 ч. на заседании диссертационного совета Д 003.021.01 в ИДСТУ СО РАН по адресу: 664033, г. Иркутск, ул. Лермонтова, 134.

С диссертацией можно ознакомиться в библиотеке и на официальном сайте wwv.idstu.irk.ru ИДСТУ СО РАН.

Автореферат разослан 13 мая 2011 г.

Ученый секретарь диссертационного совета, д.ф.-м.н. __А. А. Щеглова

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

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

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

Одним из достижений в исследовании комбинаторных проблем является прогресс в решении систем логических (булевых) уравнений большой размерности. На сегодняшний день существуют алгоритмы, которые позволяют решать системы, содержащие сотни тысяч булевых переменных и уравнений (булевых ограничений). К булевым уравнениям эффективно сводятся многочисленные комбинаторные задачи. Процедура перехода от исходной постаг новки к системе булевых уравнений называется пропозициональным кодированием. Задачи, сводящиеся к булевым уравнениям, возникают в таких областях, как синтез и верификация схем в микроэлектронике, исследование безопасности коммуникационных протоколов, обоснование корректности программ, криптоанализ, исследование свойств динамических дискретно-автоматных моделей. Отметим, что работ, посвященных пропозициональному кодированию перечисленных задач, немного в сравнении с потоком статей по алгоритмам решения булевых уравнений. Результаты по пропозициональному кодированию представлены в работах С. Прествича, Дж. Маркеса-Сильвы, Ф. Массаччи, Л. Марраро, И. Лине, И. Гента, Г. А. Опарина, В. Г. Богдановой, А. П. Новопашина, Дж. Гу, Н. Эйена, Н. Сорренсона и др.

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

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

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

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

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

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

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

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

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

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

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

Методы и инструменты исследования. Теоретическая часть исследований базируется на теории множеств, методах дискретной математики, теории булевых функций, теории вычислительной сложности, криптографии, теории процедурных языков программирования. Экспериментальная часть использует современные средства разработки программного обеспечения (язык программирования С++, среда разработки и сборки приложений Visual Studio 2008 Express Edition).

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

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

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

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

туры данных реализованы в виде программного комплекса. Таким образом, тематика диссертации соответствует пунктам 1, 2 области исследований специальности 05.13.11.

Апробация работы. Результаты диссертации докладывались и обсуждались на 5-й Международной научной конференции «Параллельные вычислительные технологии» (Москва, 2011 г.), на IX Всероссийской школе-семинаре с международным участием Sibecrypt-Ю (Тюмень, 2010 г.), на XIV Байкальской Международной школе-семинаре «Методы оптимизации и их приложения» (Северобайкальск, 2008 г.), на IX и X Всероссийских конференциях молодых ученых «Математическое моделирование и информационные технологии» (Иркутск, 2007 г., 2009 г.), на ежегодных конференциях «Ля-пуновские чтения и презентация информационных технологий» (Иркутск, 2007-2010 гг.), а также на семинарах Института динамики систем и теории управления СО РАН, Института цитологии и генетики СО РАН, Института математики им. С. Л. Соболева СО РАН, Института систем информатики им. А. П. Ершова СО РАН.

Результаты диссертации были получены в рамках следующих проектов:

- проект СО РАН «Интеллектные методы и инструментальные средства создания и анализа интегрированных распределенных информационно-аналитических и вычислительных систем для междисциплинарных исследований с применением ГИС, GRID и Веб-технологий» (№ гос. регистрации 01.2.00708582), 2007-2009 гг.;

- проекта СО РАН «Интеллектные методы автоматизации решения задач в параллельных и распределенных вычислительных средах» (№ гос. регистрации 01.2.01001348), 2010-2011 гг.;

- грант РФФИ № 07-01-00400-а «Характеризация сложности обращения дискретных функций в задачах криптографии и интервального анализа»;

грант РФФИ № 11-07-00377-а «Разработка параллельных алгоритмов решения булевых уравнений и их реализация в GRID-системах»;

- грант Президента РФ НШ-1676.2008.1.

Публикации и личный вклад автора. Наиболее значимые результаты диссертации представлены в работах [1-9], в число которых входят 4 статьи в журналах, рекомендованных ВАК РФ, 1 статья в тематическом сборнике, 2 полных текста докладов в материалах международных конференций, а также свидетельство о регистрации программы для ЭВМ.

Результаты главы 1 опубликованы в работах [4, 5]; результаты главы 2 опубликованы в [1-3]; результаты главы 3 опубликованы в [1-3, 6-8].

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

жат постановки задач и некоторые теоретические результаты. В работах [2], [6] и [8] Зашеину О. С. принадлежат результаты по распараллеливанию схем решения SAT-задач. Все результаты по разработке и реализации алгоритмов сведения комбинаторных задач к булевым уравнениям принадлежат автору.

Структура работы. Диссертация состоит из введения, трех глав, заключения, списка литературы из 121 наименования и четырех приложений. Объем диссертации — 128 страниц. Диссертация содержит 19 рисунков и 7 таблиц.

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

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

Рассматриваются алгоритмически вычислимые за полиномиальное от п время семейства функций вида

и : {0,1}" {0,1}*, dom /„ = {0,1}*, п е N.

Пропозициональное кодирование алгоритма, вычисляющего произвольную функцию /„, состоит в построении символьного описания всех возможных эволюций соответствующего вычисления на произвольных входах из {0,1}". Схематично данный процесс можно представить в следующем виде:

К1

Г

X,

1 т

»iL ••• х*>(«)

1

1

4 ХрЫ)

.....*„!

..........*Ü))=1

Рис. 1. Последовательность конфигураций памяти вычислительного устройства

Здесь К°,К1,...,Ке — последовательность конфигураций памяти вычислительного устройства (К°, Ке — начальная и заключительная конфигурации). Каждой конфигурации К' ставится в соответствие множество булевых переменных Х\ г = 0,..., е. Переменные этих множеств связаны между собой системами булевых уравнений1.

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

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

Во второй главе описаны все базовые алгоритмы и структуры данных, используемые в процессе преобразований процедурных описаний дискретных функций в булевы уравнения; приведена архитектура программного комплекса Transaig и дано описание основных его функциональных возможностей.

В разделе 2.1 представлен проблемно-ориентированный язык (язык ТА), предназначенный для описания алгоритмов, вычисляющих дискретные функции, с целью их преобразования в булевы уравнения. Язык ТА является процедурным языком с блочной структурой и С-подобным синтаксисом. Каждый блок — это список инструкций TA-программы. Программа на языке ТА представляет собой набор определений функций, а также объявлений и определений глобальных переменных и констант. В языке ТА реализованы все основные примитивные конструкции, характерные для процедурных языков программирования (объявление/определение переменной или массива переменных; определение именованных констант; определение функции; оператор присваивания; составной оператор; оператор условного перехода; оператор цикла; оператор вызова функции; оператор возврата из функции).

Язык ТА относится к языкам программирования с операционной семантикой2. Основная его особенность заключается в том, что процесс интерпретации произвольной TA-программы является по своей сути ее символьным исполнением3. Символьное исполнение предполагает расширенную семантику, в соответствии с которой выполняемая программа по множеству символов, кодирующих вход рассматриваемой функции /„, /„ : {0,1}" {0,1}*, dorn /„ = {0,1}", строит систему булевых уравнений S(fn). Подстановка в 5(/„) произвольного у £ range fn дает совместную систему Sy(fn), из произвольного решения которой можно эффективно выделить такое значение х 6 {0,1}", что fn(x) = у. Для нахождения решений системы Sy(fn) можно использовать современные булевы решатели.

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

2 Касьянов В. Н., Потгосин И. В. Методы построения трансляторов. — Новосибирск: Наука, 19S6.

344 С.

3 King J. С. Symbolic execution and program testing // Communications of the ACM. 1976. Vol. 19, №7. Pp. 385-394,

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

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

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

х\Т(иъ...,ик).

Здесь я — переменная кода, Т(щ,... ,гц)— терм исчисления высказываний над переменными кода (булевыми переменными) («|» — разделяю-

щий символ). Допустимыми операциями над переменными, имеющими тип bit, являются произвольные операции исчисления высказываний.

Процессу символьного исполнения ТА-программы соответствует последовательность конфигураций ТА-машины: К0, ...,Ке (К0 — начальная, Ке — заключительная конфигурации). Для каждого i € {0,..., е} обозначим через X1 множество переменных кода, связанных с переменными программы в конфигурации КТаким образом,

х = (]х<

— это множество всех переменных кода, введенных в процессе символьного исполнения рассматриваемой ТА-программы. Множество Х° образовано булевыми переменными, которые кодируют входные данные дискретной функции. Множество переменных кода, которые кодируют выход этой функции, будем обозначать через Y (Y С X).

Переменные программы, связанные в конфигурации К0 с переменными кода из множества Х°, объявляются в тексте ТА-программы с атрибутом _in. Переменные программы, которые в процессе символьного исполнения связываются с переменными кода из множества Y, объявляются с атрибутом _out. Переменные программы с атрибутами _in и _out — это переменные с глобальной областью видимости.

Кроме типа bit, в языке ТА используются вспомогательные типы: дело-численный тип int, представляющий четырехбайтовое знаковое целое число, а также тип bool —целое число из множества {0,1}.

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

х = Ф (хЛ,...,х,-г).

Здесь х —переменная программы, которая через структуру var_object связана с некоторой переменной кода, а Ф(х71,...,xjr) — выражение над переменными программы. Результатом интерпретации выражения Ф(х_,-и... ,Xjr) является некоторый терм ... ,xjk) над переменными кода. Затем осу-

ществляется проверка словаря Е на предмет наличия в нем терма <р. Если ip £ Е, то данный терм связывается с новой переменной кода х и добавляется в словарь Е. При этом в систему булевых уравнений добавляется уравнение вида

{х = фк,...,хк)) = 1.

Если же (р € Е, это означает, что представленная данным термом информация уже учтена в пропозициональном коде программы и ей соответствует отдельная переменная кода х'. В этом случае переменная программы х связывается с переменной кода х' через структуру var_object. Данный прием позволяет избегать ввода булевых переменных, кодирующих одну и ту же информацию.

Подраздел 2.2.2 посвящен описанию процесса интерпретации основных операторов языка ТА. Наиболее трудным этапом этого процесса является интерпретация операторов условного перехода.

Оператор условного перехода это оператор вида (в псевдокоде)

if Ф (xj,,..., xjr) then Оператор_ 1; else Оператор_2;

здесь Ф(хд,... ,xjr) — выражение над переменными программы, а Оператор_1 и Оператор_2 — произвольные операторы языка ТА (оператор присваивания,

оператор условного перехода, оператор цикла, оператор вызова функции или составной оператор). Интерпретация оператора условного перехода начинается с построения по выражению Ф терма tp над переменными кода. После этого выполняется интерпретация операторов Оператор_1 и Оиератор_2, в процессе которой строятся два альтернативных множества конфигураций ТА-машины Д1 и Дг- Данные множества образованы конфигурациями, в которых зафиксированы изменения в памяти ТА-машины, являющиеся результатами выполнения операторов Оператор_1 и Оператор_2, соответственно. Затем интерпретатор определяет множество переменных программы, которые изменили свое значение хотя бы в одной из конфигураций, представленных в Д1 и Дг- Пусть х— произвольная такая переменная, изменяющая свое значение по крайней мере в одной из конфигураций К\ и К? (К\ Е Дi, ЛГг 6 Дг)-Пусть значениями х в A'i и K<i являются слова

соответственно. Здесь х новая переменная кода, ¿1 и 62 некоторые термы над переменными кода. В результате интерпретации оператора условного перехода с переменной программы х связывается переменная кода х, в словарь термов Е добавляется терм

tp ■ Si УХр- ¿2,

а в систему булевых уравнений добавляется уравнение

(х = <р ■ ¿"1 Vtp- S2) = 1.

Далее рассматривается конструкция из нескольких вложенных операторов условного перехода (в псевдокоде).

if Фх(...) then Оператор_1; else if Ф2(...) then Оператор_2;

else if Фп(...) then Оператор_п; else Оператор_п+1;

В соответствии со сказанным выше каждое выражение Ф,, г = 1,..., п, преобразуется в терм <pi над множеством переменных кода, строится п + 1 альтернативное множество Д1,..., Дп+1 конфигураций ТА-машины и определяется множество переменных программы, каждая из которых изменила свое значение хотя бы в одной из конфигураций, представленных в Дь..., Дп+х. Пусть

х — такая переменная и ее значениями в соответствующих п + 1 альтернативных конфигурациях ТА-машины являются слова

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

VI ■ il V^i ■ щ ■ 62 V... V ft ■ ft •.. . J ■ tpn ■ 6п Vft •... ■ ft, ■ Jn+i,

а в систему булевых уравнений добавляется уравнение

(х = <pi - 6iV^-tp2 - Ô2V.. -.. 1ра - SnVlpi'... -<рп - 5n+i) = 1.

Также в этом подразделе кратко описан процесс интерпретации остальных операторов языка ТА (оператора цикла, оператора вызова функции, оператора возврата из функции).

В подразделе 2.2.4 приведены основные механизмы, используемые при преобразовании в булевы уравнения целочисленных операций. Необходимость таких преобразований возникает при работе с комбинаторными задачами, в которых фигурируют функции над целыми числами (например, в некоторых дискретных моделях генных сетей). В процессе преобразования целые числа представляются булевыми массивами, при этом в тексте ТА-программы присутствуют операции над буквенными обозначениями чисел. Например, результатом преобразования ТА-программы

__in bit a[n] ;

__in bit b[n] ;

__out bit c[n+l];

void main(H с = a + b;

>

будет система булевых уравнений следующего вида:

' (со s а0 Ф Ь0) = 1

(ро = ао • b0) = 1 _

< (pj = maj(aj, fy,Pj_i)) = 1, j = 1, n - 1

(a = ai®bi®pi-i) = l, i = i,n -1 k [Cn == Pn-l) = 1.

Запись «maj(£,y, z)» обозначает терм x-yVx-zVy-z; для кодирования битов переноса вводятся новые переменные кода р;, г = 0, п — 1. Аналогичным образом выглядят механизмы преобразования операций умножения, вычитания

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

В разделе 2.3 приведено описание программного комплекса Тгааза^, в котором были реализованы все представленные во второй главе алгоритмы и структуры данных. Здесь же описаны различные форматы выходных данных, генерируемых комплексом Тгапэа^.

Рис. 2. Архитектура программного комплекса Тгапва^

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

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

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

Помимо процедурных описаний функций на языке ТА комплекс Transalg позволяет работать с непроцедурными постановками задач 0-1-ЦЛП (0-1-иело числепное линейное программирование) и QAP (квадратичная задача о назначениях). Подробное описание механизмов преобразования данных задач в булевы уравнения приведено в третьей главе диссертации (раздел 3.3).

В комплексе Transalg переход от систем булевых уравнений к уравнениям вида КНФ=1 осуществляется при помощи преобразований Цейтина4, дополненных процедурами минимизации булевых функций в классе КНФ5. Кроме этого, предусмотрен вывод пропозиционального кода алгоритма в форме системы полиномиальных уравнений над GF(2), а также возможность построения И-НЕ-графа, представляющего алгоритм вычисления рассматриваемой функции в форме схемы из функциональных элементов над базисом {&,-■}.

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

В разделе 3.1 приведены результаты преобразования в булевы уравнения (и в конечном счете в SAT-задачи) ряда криптографических функций. Рассмотрены генераторы ключевого потока Брюера, Рюппеля и Гиффорда, а также генератор, используемый в системе шифрования А5/1. Полученный комплексом Transalg пропозициональный код генератора А5/1 позволил осуществить его успешный логический криптоанализ в GRID-системе6.

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

5 Минимизация булевых функций в комплексе TVansalg осуществляется при помощи свободно распространяемой утилиты Espresso (http://embedded.eecs.berkeley.edu/pubs/downloads/espresso).

6 Посышшн М. А., Заикян О. С., Беспалов Д. В., Семенов А. А. Решение задач криптоанализа поточных шифров в распределенных вычислительных средах // Труды ИСА РАН. 2009. Т. 46. С. 119-137.

В подразделе 3.1.4 при помощи комплекса Transalg решается задача преобразования в SAT алгоритма блочного шифрования DES. Особо подчеркнем, что данная задача положила начало целому направлению, известному сегодня как «логический криптоанализ». Одним из базовых примитивов шифра DES являются перестановки. Перестановки в DES задаются таблицами натуральных чисел, которые не являются секретными. Произвольная перестановка применяется к некоторому множеству битов обрабатываемого слова. При пропозициональном кодировании операции перестановки Transalg не создает новых переменных кода, поскольку ему достаточно обновить связи переменных программы с уже существующими элементами словаря термов Е. Данный факт означает, что операции перестановки не вносят в пропозициональный код алгоритма новой информации, никак не усложняя задачу логического криптоанализа. В результате применения комплекса Transalg к кодированию алгоритма DES был получен (см. таблицу 1) пропозициональный код (в КНФ), существенно более экономный, чем код, приведенный в работе Ф. Массаччи и JI. Марраро7.

Таблица 1. Кодирование процесса шифрования алгоритмом DES одного блока открытого текста длиной 64 бита

Программный комплекс Transalg F. Massacci, L. Маггаго

Без минимизации Минимизация

Перемепные Дизъюнкты Переменные Дизъюнкты Переменные Дизъюнкты

1912 37888 1912 26400 10336 61935

В разделе 3.2 перечислены результаты применения комплекса Transalg к исследованию поведения дискретных моделей генных сетей. Рассматривались задачи поиска циклов для одного класса дискретных автоматов, моделирующих поведение генных сетей8. Комплекс Transalg генерировал SAT-задачи по ТА-программам, описывающим динамику функционирования генной сети с дополнительными условиями на возникновение цикла определенной длины. Получаемые SAT-задачи решались известным SAT-решателем9 MiniSat 2.0. Для всех тестов либо были найдены циклы (длины до 10), либо было установлено, что таких циклов нет.

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

7 Massacci F., Маггаго L. Logical Cryptanalysis as a SAT Problem // J. of Automated Reasoning. 2000. Vol. 24,110. 1-2. Pp. 165-203.

e Евдокимов А. А., Кочемазов С. К , Семенов А. А. Применение символьных вычислений к исследованию дискретных моделей некоторых классов гепных сетей // Вычислительные технологии. 2011. Т. 16, №1. С. ЖМ7.

9 http://miuisat.se/MiniSat.htnil

тематика является сравнительно новой и интенсивно исследуемой. Преобразования осуществлялись при помощи дополнительного модуля комплекса Transalg, созданного специально для рассматриваемого класса задач. Основным авторским компонентом примененных преобразований являются процедуры декомпозиции преобразуемых выражений с последующим использованием минимизации булевых функций. Получаемые пропозициональные коды задач из семейства 0-1-ЦЛП (целочисленное линейное программирование) сравнивались с кодами, полученными известной программой10 MiniSat-K Следует отметить, что коды, построенные комплексом Transalg, содержали меньшее число переменных, но большее число дизъюнктов, чем коды, построенные программой MiniSat+. По времени решения соответствующие SAT-задачи оказались сопоставимы.

В заключительной части раздела описано преобразование в булевы уравнения известной комбинаторной проблемы — квадратичной задачи о назначениях (QAP). Данная задача известна как «одна из наиболее труднорешаемых комбинаторных проблем»11. Следует отметить, что эффективность «традиционных» (комбинирующих принципы ветвей, границ и отсечений) методов решения задач дискретной оптимизации на QAP невысока. Это требует разработки в применении к QAP новых подходов и алгоритмов. С использованием комплекса Transalg в диссертации были осуществлены сведения задач из семейства QAP к итеративному поиску решений SAT-задач.

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

В приложениях к диссертации содержится грамматика языка ТА в нотации Бэкуса-Наура, тексты некоторых ТА-программ (программа шифра DES, программа генератора А5/1 и программа, описывающая функционирование генной сети).

РЕЗУЛЬТАТЫ, ВЫНОСИМЫЕ НА ЗАЩИТУ

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

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

10 Eeu N.f Sorenssou N. Translating Pseudo-Boolean Constraints into SAT // J. on Satisfiability, Boolean Modeling and Computation. 2006. Vol. 2. Pp. 1-25.

11 Cela E. The Quadratic Assignment Problem. Theory and Algorithms. — Kluwer Academic Publishers. 1398. 287 p.

обеспечивающей эффективное построение булевых уравнений в процессе интерпретации ТА-программ.

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

4. Создан программный комплекс Тгапва^, основное назначение которого состоит в генерации булевых уравнений по процедурным описаниям дискретных функций, выполненным на языке ТА.

СПИСОК ОСНОВНЫХ ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Отпущенников И.В., Семенов А. А. Технология трансляции комбинаторных проблем в булевы уравнения /'/' Прикладная дискретная математика. 2011. № 1. С. 90-115.

2. ЗаикинО. С., Отпущенников И. В., Семенов А. А. Параллельные алгоритмы решения проблемы выполнимости в применении к оптимизационным задачам с булевыми ограничениями // Вычислительные методы и программирование: Новые вычислительные технологии (Электронный научный журнал). 2011. Т. 12. С. 205-212.

3. Отпущенников И. В., Семенов А. А. Преобразования алгоритмов вычисления дискретных функций в булевы уравнения // Известия ИГУ. Серия: математика. 2011. Том 4. № 1. С. 83-96.

4. Семенов А. А., Отпущенников И. В., Кочемазов С. Е. Пропозициональный подход в задачах тестирования дискретных автоматов // Современные технологии. Системный анализ. Моделирование. 2009. № 4. С. 48-56.

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

6. Семенов А. А., ЗаикинО. С., Отпущенников И. В., Буров П. С. О некоторых особенностях задач обращения дискретных функций // Труды XIV Байкальской Международной школы-семинара «Методы оптимизации и их приложения». - Иркутск: ИСЭМ СО РАН. 2008. Т. 1. С. 498-505.

7. Отпущенников И. В., Семенов А. А. Программная трансляция алгоритмов в пропозициональную логику применительно к комбинаторным задачам // Прикладная дискретная математика. Приложение. 2010. № 3. С. 81-82.

8. Занкин О. С., Отпущенников И. В., Семенов А. А. Параллельные алгоритмы решения SAT в применении к оптимизационным задачам с булевыми ограничениями // Труды V Международной конференции «Параллельные вычислительные технологии» (ПАВТ 2011). Москва, МГУ. 2011. С. 501-508.

9. Отпущенников И. В., Семенов А. А. Инструментальное средство трансляции алгоритмов вычисления дискретных функций в выражения исчисления высказываний Transalg 1.0. Свидетельство о государственной регистрации программы для ЭВМ № 2011611151 (03.02.2011).

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

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

Введение

Глава 1. Пропозициональное кодирование формальных вычислительных моделей.

1.1. Базовые понятия и определения.

1.2. Пропозициональное кодирование программ для формальных вычислительных моделей.

1.2.1. Механизмы преобразования в булевы уравнения ИАМ-программ, вычисляющих дискретные функции

1.2.2. Преобразования Цейтина.

1.3. Основные алгоритмы решения систем булевых уравнений

1.4. Необходимость разработки методов и средств преобразования процедурных описаний алгоритмов в булевы уравнения

Глава 2. Преобразование процедурных описаний дискретных функций в булевы уравнения.

2.1. Описание проблемно-ориентированного языка ТА.

2.2. Интерпретация ТА-программ. Формирование пропозиционального кода алгоритма.

2.2.1. Базовые механизмы символьного исполнения ТА-программ

2.2.2. Символьное исполнение основных операторов языка

2.2.3. Процедура декомпозиции сложных термов.

2.2.4. Преобразование операций над целыми числами

2.3. Программный комплекс Тгапва^ для преобразования алгоритмов вычисления дискретных функций в булевы уравнения

Глава 3. Результаты преобразования в булевы уравнения алгоритмов вычисления некоторых дискретных функций 70 3.1. Преобразование в булевы уравнения некоторых криптографических функций

3.1.1. Преобразование в булевы уравнения алгоритма генератора ключевого потока шифра А5/1.

3.1.2. Преобразование в булевы уравнения алгоритма суммирующего генератора.

3.1.3. Преобразование в булевы уравнения алгоритма генератора Гиффорда.

3.1.4. Преобразование в булевы уравнения алгоритма DES

3.1.5. Преобразование в булевы уравнения алгоритма хеширования MD5.

3.2. Исследование свойств дискретно-автоматных динамических систем.

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

3.3.1. Сведение к SAT задач 0-1-целочисленного линейного программирования.

3.3.2. Сведение к SAT квадратичных задач о назначениях (QAP)

Актуальность темы исследования. Интенсивное развитие вычислительных технологий, наблюдающееся в последние годы, сделало возможным решение комбинаторных задач таких размерностей, которые раньше казались непреодолимыми. Следствием этого стало появление новых направлений в вычислительных разделах дискретной математики и математической логики. Как известно, подавляющее число практически значимых комбинаторных задач являются МР-трудными в общей постановке. Данное обстоятельство тем не менее не следует рассматривать как непреодолимое препятствие, поскольку во многих случаях тщательный анализ проблемы и правильный выбор алгоритмов и технологий позволяют найти решение за приемлемое время.

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

Можно сослаться на результаты пропозиционального кодирования, представленные в статьях С. Прествича, Дж. Маркеса-Сильвы, Ф. Массаччи, Л. Марраро, И. Лине, И. Гента, Г. А. Опарина, В. Г. Богдановой, А. П. Но-вопашина, Дж. Г у, Н. Эйена, Н. Сорренсона и некоторых других авторов [1-12].

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

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

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

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

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

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

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

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

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

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

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

Методы и инструменты исследования. Теоретическая часть исследований базируется на теории множеств, методах дискретной математики, теории булевых функций, теории вычислительной сложности, криптографии, теории процедурных языков программирования. Экспериментальная часть использует современные средства разработки программного обеспечения (язык программирования С++, среда разработки и сборки приложений Visual Studio 2008 Express Edition).

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

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

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

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

Содержательная часть работы включает введение и три главы.

Первая глава посвящена основам методологии преобразования в булевы уравнения процедур вычисления дискретных функций в контексте формальной вычислительной модели — двоичной машины с произвольным доступом к памяти (RAM). Описываются основные механизмы построения булевых уравнений по программе для двоичной RAM.

В разделе 1.1 вводятся основные понятия и определения, дается общая формулировка задачи обращения дискретных функций.

В разделе 1.2 приведена основная теорема об эффективной сводимости проблемы обращения полиномиально вычислимых дискретных функций к задачам поиска решений систем булевых уравнений. Здесь же описаны преобразования Цейтина — основной инструмент перехода от произвольных систем булевых уравнений к уравнениям в нормальных формах.

В разделе 1.3 проводится краткий обзор основных методов решения булевых уравнений.

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

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

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

Раздел 2.2 посвящен описанию основных механизмов интерпретации ТА-программ (семантике языка ТА). В соответствии с принятым подходом [13] интерпретационная семантика языка ТА описывается через ввод в рассмотрение абстрактной машины языка ТА (ТА-машины). Произвольная конфигурация ТА-машины фиксирует момент интерпретации некоторой инструкции ТА-программы. При этом в памяти ТА-машины отображается информация о связи переменных, фигурирующих в тексте ТА-программы, с переменными, фигурирующими в системе булевых уравнений, и с логическими выражениями (термами). Здесь же описывается техника сокращения избыточности пропозиционального кода алгоритма, использующая специальный словарь термов. В этом же разделе подробно описаны механизмы символьной интерпретации основных операторов языка ТА. В заключительной части раздела рассмотрены преобразования в булевы уравнения операций над целыми числами.

В разделе 2.3 приведено описание программного комплекса Transalg, в котором были реализованы все алгоритмы и структуры данных, представленные во второй главе. Основное назначение комплекса Transalg состоит в преобразовании описаний алгоритмов вычисления дискретных функций на языке ТА в булевы уравнения. В этом же разделе описаны различные форматы выходных данных, генерируемых комплексом Transalg по ТА-про-граммам.

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

В разделе 3.1 приведены результаты преобразования в булевы уравнения (и в конечном счете в SAT-задачи) ряда криптографических функций. Рассмотрены генераторы ключевого потока Рюппеля, Гиффорда, генератор, используемый в шифре А5/1, блочный шифр DES и алгоритм хеширования MD5.

В разделе 3.2 комплекс Transalg используется для построения SAT-задач, кодирующих проблемы поиска циклов автоматных отображений, описывающих поведение дискретных динамических моделей генных сетей [14,15]. Получаемые SAT-задачи решались известным SAT-решателем Mini

Sat 2.0 [16]. Для всех тестов либо были найдены циклы (длины до 10), либо было установлено, что таких циклов нет.

В разделе 3.3 приведено описание дополнительных модулей комплекса Transalg, предназначенных для сведения задач с псевдобулевыми ограничениями к SAT-задачам. При помощи программного комплекса Transalg к SAT-задачам были сведены задачи из семейства 0-1-ЦЛП (целочисленное линейное программирование) и задачи из семейства QAP (квадратичная задача о назначениях).

В Приложении 1 описана грамматика языка ТА в нотации Бэкуса-На-ура. Приложение 2 содержит ТА-программу, вычисляющую 100 бит ключевого потока генератора А5/1. В Приложение 3 приводится текст ТА-про-граммы, описывающей алгоритм вычисления криптографической функции DES. Приложение 4 содержит пример ТА-программы, моделирующей функционирование генной сети.

Апробация работы. Результаты диссертации докладывались и обсуждались на 5-й Международной научной конференции «Параллельные вычислительные технологии» (Москва, 2011 г.), на IX Всероссийской школе-семинаре с международным участием Sibecrypt-10 (Тюмень, 2010 г.), на XIV Байкальской международной школе-семинаре «Методы оптимизации и их приложения» (Северобайкальск, 2008 г.), на IX и X Всероссийских конференциях молодых ученых «Математическое моделирование и информационные технологии» (Иркутск, 2007 г., 2009 г.), на ежегодных конференциях «Ляпуновские чтения и презентация информационных технологий» (Иркутск, 2007-2010 гг.), а также на семинарах Института динамики систем и теории управления СО РАН, Института цитологии и генетики СО РАН, Института математики им. С. Л. Соболева СО РАН, Института систем информатики им. А. П. Ершова СО РАН.

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

• проект СО РАН «Иителлектные методы и инструментальные средства создания и анализа интегрированных распределенных информационно-аналитических и вычислительных систем для междисциплинарных исследований с применением ГИС, GRID и Веб-технологий» (№ гос. регистрации: 01.2.00708582) 2007-2009 гг.;

• проекта СО РАН «Иителлектные методы автоматизации решения задач в параллельных и распределенных вычислительных средах» (№ гос. регистрации: 01201001348), 2010-2011 гг.;

• грант РФФИ № 07-01-00400-а «Характеризация сложности обращения дискретных функций в задачах криптографии и интервального анализа»;

• грант РФФИ № 11-07-00377-а «Разработка параллельных алгоритмов решения булевых уравнений и их реализация в GRID-системах»;

• грант Президента РФ НШ-1676.2008.1.

Публикации и личный вклад автора. По теме диссертации опубликовано 12 работ. Наиболее значимые результаты представлены в [17-25]. В число указанных работ входят 4 статьи из Перечня ведущих рецензируемых журналов и изданий ВАК РФ (от 25.02.2011 г.), 1 статья в тематическом сборнике, 2 полных текста докладов в материалах международных конференций, а также одно свидетельство о регистрации программы для ЭВМ.

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

18], [23] и [24] Заикину О. С. принадлежат результаты по распараллеливанию схем решения ЭАТ-задач. Все результаты по разработке и реализации алгоритмов сведения комбинаторных задач к булевым уравнениям принадлежат автору.

Структура работы. Диссертация состоит из введения, трех глав, заключения, списка литературы из 121 наименования и четырех приложений. Объем диссертации — 128 страниц. Диссертация содержит 19 рисунков и 7 таблиц.

Основные выводы по третьей главе. Описанный во второй главе комплекс Transalg применялся для преобразования в булевы уравнения ТА-программ, описывающих функционирование разнообразных дискретных систем. В большинстве случаев результатом такого преобразования является пропозициональный код алгоритма вычисления дискретной функции в виде уравнения КНФ—1. В получаемых КНФ входные и выходные данные рассматриваемой функции представлены булевыми переменными. Такие КНФ называются шаблонными (шаблонами). SAT-задача, кодирующая проблему обращения функции в конкретной точке у Е range fn получается в результате приписывания (по конъюнкции) к шаблонной КНФ однолитеральных дизъюнктов, кодирующих слово у. Получаемая КНФ подается на вход SAT-решателю. Из ее выполняющего набора эффективно извлекается такое слово х е {0,1}п, что fn(x) — у.

В результате применения комплекса Transalg была построена библиотска шаблонов (в виде КНФ, представленных в формате DIMACS [104]), кодирующих задачи обращения ряда криптографических функций (алгоритм DES, генератор А5/1, суммирующий генератор, генератор Гиффорда, генератор Геффе, алгоритм хеширования MD5). В построенную библиотеку шаблонов также включены КНФ, кодирующие задачи 0-1-ЦЛП, QAP и задачи поиска циклов для некоторых дискретно-автоматных динамических моделей генных сетей.

Заключение

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

Далее перечислены основные результаты диссертации:

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

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

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

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

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

1. Prestwich S. D. CNF encodings. 1. Handbook of Satisfiability (editors: A. Biere, M.Heule, H. van Maaren, T.Walsh). 2009. Vol. 6. pp. 75-97.

2. Marques-Silva J., Lynce I. Towards robust cnf encodings of cardinality constraints //In Thirteenth International Conference on Principles and Practice of Constraint Programming. Springer. Lecture Notes in Computer Science. 2007. Vol. 4741. pp. 483-497.

3. Massacci F., Marraro L. Logical Cryptanalysis as a SAT Problem // Journal of Automated Reasoning. 2000. Vol. 24, no. 1-2. pp. 165-203.

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

5. Gent I. P., Lynce I. A sat encoding for the social golfer problem // In Workshop on Modelling and Solving Problems with Constraints, IJCAI'05. 2005.

6. Gent I.P., Nightingale P. A new encoding of alldiffercnt into sat // In Third International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, CP'04. 2004.

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

8. Опарин Г. А., Новопашин А. П. Булево моделирование планированиядействий в распределенных вычислительных системах // Известия РАН. Теория и системы управления. 2004. № 5. С. 105-108.

9. Oparin G.A., Novopashin А. P. Boolean models and planning methods for parallel abstract programs // Automation and Remote Control. 2008. Vol. 69, no. 8. pp. 1423-1432.

10. Опарин Г. А., Новопашин А. П. Булевы модели синтеза параллельных планов решения вычислительных задач // Вестник НГУ. Серия: Информационные технологии. 2008. Т. 6, № 1. С. 53-59.

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

12. Een N., Sorrensson N. Translating Pseudo-Boolean Constraints into SAT // Journal on Satisfiability, Boolean Modeling and Computation. 2006. Vol. 2. pp. 1-25.

13. Касьянов В. H., Поттосин И. В. Методы построения трансляторов. Новосибирск: «Наука», 1986. С. 344.

14. Григоренко Е. Д., Евдокимов А. А., Лихошвай В. А., Лобарева И. А. Неподвижные точки и циклы автоматных отображений, моделирующих функционирование генных сетей // Вестник Томского гос. ун-та. Приложение. 2005. Т. 14. С. 206-212.

15. Системная компьютерная биология, Под ред. Н. А. Колчанова, С. С. Гончарова, В. А. Лихошвая, В. А. Иванисенко. Новосибирск: Изд-во СО РАН, 2008. С. 767.

16. MiniSat. URL: http://minisat.se/MiniSat.html (дата обращения: 10.05.2011).

17. Отпущенников И.В., Семенов A.A. Технология трансляции комбинаторных проблем в булевы уравнения // Прикладная дискретная математика. 2011. № 1. С. 96-115.

18. Отпущенников И.В., Семенов A.A. Преобразования алгоритмов вычисления дискретных функций в булевы уравнения // Известия ИГУ. Серия: математика. 2011. Т. 4, № 1. С. 83-96.

19. Семенов A.A., Отпущенников И. В., Кочсмазов С. Е. Пропозициональный подход в задачах тестирования дискретных автоматов // Современные технологии. Системный анализ. Моделирование. 2009. № 4. С. 48-56.

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

21. Отпущенников И. В., Семенов А. А. Программная трансляция алгоритмов в пропозициональную логику применительно к комбинаторным задачам // Прикладная дискретная математика. Приложение. 2010. № 3. С. 81-82.

22. Отпущенников И. В., Семенов А. А. Инструментальное средство трансляции алгоритмов вычисления дискретных функций в выражения исчисления высказываний Transaig 1.0. Свидетельство о государственной регистрации программы для ЭВМ № 2011611151 (03.02.2011).

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

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

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

26. Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. Москва: «Мир», 1982. С. 416.

27. Пападимитриу X., Стайглиц К. Комбинаторная оптимизация. Алгоритмы и сложность. Москва: «Мир», 1985. С. 510.

28. Васильев Ю. Л., Ветухновский Ф. Я., Глаголев В. В. и др. Дискретная математика и математические вопросы кибернетики. Москва: «Наука», 1974. Т. 1.

29. Нигматуллин Р. Г. Сложность булевых функций. Москва: «Наука», 1991. С. 240.

30. Wegener I. The complexity of Boolean function. Stuttgart: J. Wiley and Sons ltd, 1987.

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

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

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

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

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

36. Nemhauser G., Wolsey L. Integer and Combinatorial Optimization. John Wiley and Sons Ltd., 1998.

37. Cela E. The Quadratic Assignment Problem. Theory and Algorithms. Kluwer Acadcmic Publishers, 1998. P. 287.

38. Schrijver A. Combinatorial Optimization. Springer Verlag, Berlin, 2003.

39. Cook S. A. The complexity of theorem-proving procedures // Proceedings of the third Annual ACM Symposium on Theory of Computing. 1971. Vol. 35, no. 8. pp. 151-159.

40. Shepherdson J.C., Sturgis H. E. Computability of recursive functions // J. Assoc. Сотр. Machinery. 1963. Vol. 10. pp. 217-255.

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

42. Menezes A., van Oorshot P., Vanstone S. Handbook of Applied Cryptography. CRC Press, 1996. P. 657.

43. Schneier B. Applied Cryptography, Second Edition: Protocols, Algorithms, and Source Code in C. John Wiley and Sons, 1996. P. 758.

44. Лидл P., Нидеррайтер Г. Конечные поля (в двух томах). Москва: «Мир», 1988.

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

46. Семенов А. А. О преобразованиях Цейтина в логических уравнениях // Прикладная дискретная математика. 2009. № 4. С. 28-50.

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

48. Tseitin G. On the complexity of derivation in prepositional calculus // Automation of reasoning. 1983. Vol. 2. pp. 466-483.

49. Hachtel G.D., Somenzi F. Logic synthesis and verification algorithms. Kluwer Ac. Publ., 2002.

50. Черемисинова Jl. Д., Новиков Д. Я. Проверка схемной реализации частичных булевых функций // Вестник Томского гос. ун-та. Управление, вычислительная техника, информатика. 2008. № 4 (5). С. 102-111.

51. Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification. URL: http://www.eecs.berkeley.edu/alanmi/abc/ (дата обращения: 10.05.2011).

52. Kuehlmann A., Cornelis A. J., van Eijk. Combinational and Sequentional Equivalence Checking // Logic synthesis and Verification, Ed. by S. Hassoun, T. Sasao, R. K. Brayton. Kluwer Academic Publishers, 2002. pp. 343-372.

53. Advanced Formal Verification // Ed. by R. Drechsler. Springer, 2005. P. 280.

54. Ganai M., Gupta A. SAT-based scalable formal verification solutions. Springer, 2007. P. 326.

55. Boole G. An investigation of the laws of thought on which are founded the mathematical theories of logic and probabilities. London, 1854.

56. Rudeanu S. Boolean functions and equations. Amsterdam-London: North-Holland Publ. Сотр., 1974. P. 442.

57. Akers S.B. On a theory of Boolean functions //J. Soc. Ind. Appl. Math. 1959. Vol. 7, no. 4. pp. 487-498.

58. Buttner W., Simonis H. Embedding Boolean expressions into logic programming // Journal of Symbolic Computation. 1987. Vol. 4. pp. 191-205.

59. Brown F. M. Boolean Reasoning: The Logic Of Boolean Equations. Dover Publications, 2003. P. 304.

60. Бохмапп Д., Постхоф X. Двоичные динамические системы. Москва: «Энергоатомиздат», 1986. С. 401.

61. Семенов А. А., Буранов Е. В. Погружение задачи криптоанализа симметричных шифров в пропозициональную логику // Вычислительные технологии (совместный выпуск с журналом «Региональный вестник Востока»), 2003. Т. 8. С. 118-126.

62. Buchberger В. Grobner-Bases: An Algorithmic Method in Polynomial Ideal Theory // Multidimensional Systems Theory. 1985. Vol. 6. pp. 184-232.

63. Кокс Д., Литтл Д., О'Ши Д. Идеалы, многообразия и алгоритмы. Москва: «Мир», 2000. С. 687.

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

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

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

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

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

69. Bryant R. Е. Graph-Based Algorithms for Boolean Function Manipulation // IEEE Transactions on Computers. 1986. Vol. 35, no. 8. pp. 677-691.

70. Bryant R. E. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams // ACM Computing Surveys. 1992. Vol. 24, no. 3. pp. 293-318.

71. Meinel C., Theobald T. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications. Springer-Verlag, 1998.

72. Davis M., Logemann G., Loveland D. A machine program for theoremproving // Communications of the ACM. 1962. Vol. 5, no. 7. pp. 394-397.

73. Marques-Silva J. P., Sakallah K. A. GRASP: A search algorithm for propositional satisfiability // IEEE Transactions on Computers. 1999. Vol. 48, no. 5. pp. 506-521.

74. Zhang L., Madigan C.F., Moskewicz M.H., Malik S. Efficient conflict driven learning in a boolean satisfiability solver // In Proceedings of International Conference on Computer-Aided Design. 2001. pp. 279-285.

75. Goldberg E., Novikov Y. Berkmin: The Fast and Robust SAT Solver // Automation and Test in Europe (DATE). 2002. pp. 142-149.

76. Prestwich S.D. Sat problems with chains of dependent variables // Discrete Applied Mathematics. 2002. Vol. 3037. pp. 1-2.

77. Crawford J. M., Baker А. В. Experimental results on the application of satisfiability algorithms to scheduling problems // In Twelfth National Conference on Artificial Intelligence. AAAI Press. 1994. Vol. 2. pp. 1092-1097.

78. Ernst M., Millstein T., Weld D. Automatic sat-compilation of planning problems //In Fifteenth International Joint Conference on Artificial Intelligence. 1997. pp. 1169-1176.

79. Опарин Г. А., Богданова В. Г. РЕБУС — интеллектуальный решатель комбинаторных задач в булевых ограничениях // Вестник НГУ. Серия: Информационные технологии. 2008. Т. 6, № 1. С. 60-68.

80. Gent I. P. Arc consistency in sat. IOS Press, 2002. pp. 121-125.

81. Kasif S. On the parallel complexity of discrete relaxation in constraint satisfaction networks // Artificial Intelligence. 1990. Vol. 45. pp. 275-286.

82. Walsh T. Sat vs CSP // Lecture Notes in Computer Science. 2000. Vol. 1894. pp. 441-456.

83. Bessiere C., Hebrard E., Walsh T. Local consistencies in sat // Lecture Notes in Computer Science. 2003. Vol. 2919. pp. 229-314.

84. Bacchus F. Gac via unit propagation // Lecture Notes in Computer Science. 2007. Vol. 4741. pp. 133-147.

85. Сергиепко A. M. VHDL для проектирования вычислительных устройств. Изд-во ТИД «ДС», 2003. С. 208.

86. Поляков А. К. Языки VHDL и Verilog в проектировании цифровой аппаратуры. Москва: СОЛОН — Пресс, 2003. С. 320.

87. King J. С. Symbolic execution and program testing // Communications of the ACM. 1976. Vol. 19, no. 7. pp. 385-394.

88. Hansen Т., Schachte P., Sondergaard H. State joining and splitting for the symbolic execution of binaries // Springer-Verlag Berlin Heidelberg. 2009. pp. 76-92.

89. Abstract Interpretation, MIT course. URL: http://web.mit.edu/afs/ athena.mit.edu/course/16/16.399/www (дата обращения: 10.05.2011).

90. Bagnara R., Hill P. M., Pescetti A., Zaffanella E. On the design of generic static analyzers for imperative languages. 2007. arXiv:cs/0703116v2 cs.PL].

91. Wichmann В., Canning A., Cluttcrbuck D. L. et al. Industrial Perspective on Static Analysis // Software Engineering Journal. 1995. Vol. 10, no. 2. pp. 69-75.

92. Ayewah N., Hovemeyer D., Morgenthaler J. D. et al. Using Static Analysis to Fing Bugs // IEEE Software. 2008. Vol. 25, no. 5. pp. 22-29.

93. Ершов А. П. Проблемно-ориентированный язык программирования // Математическая энциклопедия. 1977-1985.

94. Ахо А., Сети Р., Ульман Д. Компиляторы. Принципы, технологии, инструменты. Москва, СПб, Киев: «Вильяме», 2001. С. 768.

95. Ахо А., Ульман Д. Теория синтаксического анализа, перевода и компиляции. Москва: «Мир», 1977.

96. Карпов Ю. Г. Теория и технология программирования. Основы построения трансляторов. СПб: БХВ-Петербург, 2005. С. 272.

97. Керниган Б.У., Ритчи Д. М. Язык программирования С. М.: «Вильяме», 2006. С. 304.

98. Лавров С. С. Программирование. Математические основы, средства, теория. СПб: БХВ-Петербург, 2001. С. 314.

99. Себеста Р. У. Основные концепции языков программирования. М.: «Вильяме», 2001. С. 672.

100. Espresso. URL: http://embedded.eecs.berkeley.edu/pubs/downloads /espresso (дата обращения: 10.05.2011).

101. DIMACS. URL: http://www.satalia.com/technology/cnf/ (дата обращения: 10.05.2011).

102. Biere A. The AIGER And-Inverter Graph (AIG) Format Version 20070427 // Johannes Kepler University. 2007. URL: http://fmv.jku.at/aiger/ (дата обращения: 10.05.2011).

103. Cook S., Mitchel D. G. Finding hard instances of the satisfiability problem: A survey // DIMACS Series in Discrete Mathematics and Theoretical Computer Science. 1997. Vol. 35. pp. 1-17.

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

105. Посыпкин М.А., Заикин О. С., Беспалов Д. В., Семенов А. А. Решение задач криптоанализа поточных шифров в распределенных вычислительных средах // Труды ИСА РАН. 2009. Т. 46. С. 119-137.

106. 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. Vol. 2. pp. 260-272.

107. Gifford D.IC., Lucassen J.M., Berlin S.T. The Application of Digital Broadcast Communication to Large Scale Information Systems / / IEEE Journal on Selected Areas in Communications. 1985. Vol. 3, no. 3. pp. 457-467.

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

109. Cain T.R., Sherman А. Т. How to break Gifford's Cipher // CRYPTOLOGIA. 1997. Vol. 21, no. 3. pp. 237-286.

110. Biham E., Shamir A. Differential Cryptaanalysis of DES-like Cryptosystems // Advances in Cryptology- CRYPTO 90 Proceeding, Springer-Verlag. 1991. pp. 2-21.

111. Guneysu Т., Kasper Т., Novotny M. et al. Cryptanalysis with COPACOBANA // IEEE Transactions on computers. 2008. Vol. 57, no. 11. pp. 1498-1513.

112. Rivest L. R. The MD5 Message Digest Algorithm, RFC 1321. 1992. URL: http://rfc.com.ru/rfcl321.htm (дата обращения: 10.05.2011).

113. Евдокимов А. А., Кочемазов C.E., Семенов А. А. Применение символьных вычислений к исследованию дискретных моделей некоторых классов генных сетей // Вычислительные технологии. 2011. Т. 16, № 1. С. 30-47.

114. Евдокимов А. А., Лихошвай В. А., Комаров А. В. О восстановлении структуры дискретных моделей функционирования сетей / / Вестник Томского гос. ун-та. Приложение. 2005. Т. 14. С. 213-217.

115. The International Pseudo-Boolean Competition. URL: http://www. cril.univ-artois.fr/PB10 (дата обращения: 10.05.2011).

116. CPLEX Solver. URL: http://www.aimms.com/features/solvers/ cplex (дата обращения: 10.05.2011).

117. MIPLIB Mixed Integer Problem Library. URL: http://miplib.zib.de (дата обращения: 10.05.2011).

118. MiniSat+. URL: http://minisat.se/MiniSat+.html (дата обращения: 10.05.2011).