авторефераты диссертаций БЕСПЛАТНАЯ  БИБЛИОТЕКА

АВТОРЕФЕРАТЫ КАНДИДАТСКИХ, ДОКТОРСКИХ ДИССЕРТАЦИЙ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ

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

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

Игнатьев Алексей Сергеевич

МЕТОДЫ ОБРАЩЕНИЯ ДИСКРЕТНЫХ ФУНКЦИЙ

С ПРИМЕНЕНИЕМ ДВОИЧНЫХ РЕШАЮЩИХ

ДИАГРАММ

05.13.18 – Математическое моделирование, численные методы

и комплексы программ

АВТОРЕФЕРАТ

диссертации на соискание ученой степени

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

Иркутск – 2010

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

Научный руководитель: кандидат технических наук, доцент Семенов Александр Анатольевич

Официальные оппоненты: доктор физико-математичеких наук, профессор Перязев Николай Алексеевич кандидат физико-математических наук, доцент Панкратова Ирина Анатольевна

Ведущая организация: Институт математики им. С. Л. Соболева СО РАН

Защита состоится 18 июня 2010 г. в 14:00 на заседании диссертационного со вета Д 212.074.01 при ГОУ ВПО Иркутский государственный университет по адресу: 664003, г. Иркутск, бульвар Гагарина, 20, Институт математики, экономики и информатики.

С диссертацией можно ознакомиться в библиотеке Иркутского государствен ного универститета (г. Иркутск, бульвар Гагарина, 24).

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

Ученый секретарь диссертационного совета, канд. физ.-мат. наук, доцент Антоник В. Г.

Общая характеристика работы

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

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

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

http://jsat.ewi.tudelft.nl/), подавляющее большинство статей в кото ром посвящено SAT-задачам (SAT-задачами называются задачи поиска ре шений логических уравнений вида КНФ=1).

На данный момент можно выделить (в качестве наиболее успешных) два общих подхода к поиску решений логических уравнений, высокая эффектив ность которых делает их широко используемыми. В первую очередь речь идет о SAT-подходе, в основе которого лежат процедуры приведения разнородных систем логических уравнений к уравнениям вида КНФ=1. Второй класс ме тодов базируется на использовании двоичных решающих диаграмм (BDD), а точнее сокращенных упорядоченных BDD или ROBDD формата пред ставления булевых функций в виде направленных помеченных графов специ ального вида. О популярности ROBDD-подхода в задачах синтеза и вери фикации дискретных систем говорит тот факт, что на протяжении ряда лет ключевая статья по алгоритмике двоичных решающих диаграмм1 лидирова ла в рейтинге цитируемости международной системы мониторинга научных публикаций Citeseer (см. http://citeseer.ist.psu.edu/source.html).

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



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

Исходя из всего вышесказанного, актуальными представляются пробле мы разработки, обоснования эффективности и программной реализации мето дов решения логических уравнений, в которых сочетались бы преимущества скорости обработки данных, присущей SAT-подходу, и компактности пред ставления данных, присущей ROBDD-подходу. Решатели, базирующиеся на таких методах, могут использоваться при исследовании широкого класса дис Bryant R. E. Graph-Based Algorithms for Boolean Function Manipulation // IEEE Transactions on Computers. 1986. Vol. 35, no 8. Pp. 677–691.

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

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

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

1. Разработать стратегию логического вывода, в которой SAT-подход соче тается с ROBDD-подходом в следующем смысле: DPLL (как базовый ал горитм решения SAT) порождает массивы ограничений-дизъюнктов, ко торые в дальнейшем хранятся и обрабатываются в форме ROBDD-пред ставлений соответствующих булевых функций (данный шаг предполага ет сокращение объема оперативной памяти, используемой для хранения накопленных ограничений);

разработать и реализовать ROBDD-анало ги основных механизмов вывода, используемых в современных SAT решателях;

строго обосновать корректность и эффективность работы соответствующих процедур.

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

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

разработать параллельные гибрид ные (SAT+ROBDD)-алгоритмы решения логических уравнений и обра щения дискретных функций;

программно реализовать разработанные алгоритмы с использованием стандарта MPI (Message Passing Interface);

интегрировать все разработанные алгоритмы в программный комплекс.

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

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

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

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

• ROBDD-аналоги базовых алгоритмов и процедур, используемых в со временных DPLL-решателях, а также новый алгоритм модификации порядка означивания переменных в ROBDD;

• программный комплекс, включающий ROBDD-решатель систем логи ческих уравнений, а также параллельную и последовательную версии гибридного (SAT+ROBDD)-решателя;





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

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

1. Метод обращения полиномиально вычислимых дискретных функций, в основе которого лежит гибридный (SAT+ROBDD) логический вывод;

строгое обоснование (в форме теорем) математических свойств ROBDD, рассматриваемых в роли баз булевых ограничений;

ROBDD-аналоги основных процедур, используемых в нехронологическом DPLL-выводе (правило единичного дизъюнкта, процедура Clause Learning, проце дуры работы с дизъюнктами, использующие идеологию отсроченных вычислений ).

2. Новые эвристические алгоритмы решения систем логических уравне ний, использующие двоичные решающие диаграммы (ROBDD).

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

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

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

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

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

Апробация работы. Результаты диссертации докладывались и обсуж дались на 3-ей Международной научной конференции Параллельные вычис лительные технологии (Нижний Новгород, 2009 г.);

на VII Всероссийской конференции с международным участием Новые информационные техноло гии в исследовании сложных структур (Томск, 2008 г.);

на Всероссийской школе-семинаре с международным участием Sibecrypt-09 (Омск, 2009 г.);

на VIII и на IX школах-семинарах Математическое моделирование и информа ционные технологии (Иркутск, 2006, 2007 гг.), на ежегодных конференциях из серии Ляпуновские чтения (Иркутск, 2006, 2007, 2008, 2009 гг.), а также на научных семинарах Института динамики систем и теории управления СО РАН, научных семинарах кафедры математической информатики Восточно Сибирской государственной академии образования;

научном семинаре лабо ратории дискретного анализа Института математики им. С. Л. Соболева СО РАН;

научном семинаре кафедры защиты информации и криптографии Том ского государственного университета.

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

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

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

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

Публикации и личный вклад автора. По теме диссертации опуб ликовано 14 работ. Наиболее значимые результаты представлены в работах [1–7]. В число указанных работ входят 2 статьи [1, 2] из Перечня ведущих рецензируемых журналов и изданий ВАК РФ (2010 г.), 3 статьи [3–5] в науч ных журналах, 2 полных текста докладов [6, 7] в материалах международных конференций.

Результаты, относящиеся к разделу 2.3, получены совместно с научным руководителем Семеновым А. А. и являются неделимыми. Из совместных ра бот с Беспаловым Д. В., Заикиным О. С., Хмельновым А. Е. в диссертацию включены результаты, принадлежащие лично автору.

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

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

В этой же главе сформулирована основная проблема, исследуемая в дис сертации и состоящая в следующем. Рассматривается натуральное семей ство, образованное всюду определенными дискретными функциями вида fn :

{0, 1}n {0, 1}, вычислимыми за полиномиальное от n время. Проблемой обращения произвольной функции fn из данного семейства в точке y называ ется следующая задача: по известному y range fn и известному алгоритму вычисления fn требуется найти такой x {0, 1}n, что fn (x) = y. Данная проблема может быть эффективно сведена к задаче поиска выполняющего набора КНФ C(f ) над множеством булевых переменных X = {x1,..., xp(n) }, p(·) некоторый полином.

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

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

Рассматривается произвольная система (кратко обозначаемая через S) логических уравнений вида L1 (x1,..., xn ) = ··· S:

Lm (x1,..., xn ) = Здесь Lj (x1,..., xn ), j {1,..., m}, формулы исчисления высказываний (ИВ), X = {x1,..., xn } множество булевых переменных. Характеристиче ской функцией системы S называется булева функция S : {0, 1}n {0, 1}, заданная формулой L1 (x1,..., xn ) ·... · Lm (x1,..., xn ).

Несложно понять, что по ROBDD-представлению B (S ) функции S проблема совместности системы S, а также проблема поиска некоторого ее решения могут быть решены за линейное от |B (S )| время (|B (S )| чис ло вершин в B (S )). При построении B (S ) можно использовать различ ные эвристики организации порядка означивания переменных, а также стро ить декомпозиции исходной системы с целью разбиения процесса построения B (S ) на независимые этапы. В диссертации для этих целей предложена но вая эвристическая процедура разбиения системы S на подсистемы, называе мые слоями. Пусть выбран некоторый порядок означивания переменных из X = {x1,..., xn }, : xi1 xi2... xin1 xin, в соответствии с которым предполагается строить B (S ). Число r {1,..., n} называем индексом пе ременной xir относительно выбранного порядка. Используя порядок, разби ваем систему S на слои. Первый слой образован всеми уравнениями системы, в которые входит переменная xi1. Второй слой образован всеми оставшими ся уравнениями, содержащими переменную xir, которая имеет наименьший относительно индекс по всем уравнениям, не входящим в первый слой. И так далее. Пусть R число определяемых описанным образом слоев системы.

Очевидно, что 1 R n. ROBDD каждого слоя Bj, j {1,..., R}, строится в соответствии с порядком по следующей рекурсивной схеме, использующей алгоритм Apply Р. Брайанта:

Bj = Apply Bj1 · Apply Bj2 ·... · Apply Bjk1 · Bjk, где Bj1,..., Bjk ROBDD булевых функций, выраженных формулами в ле вых частях уравнений системы, образующих j-тый слой. Итоговая ROBDD характеристической функции системы строится в соответствии с порядком по аналогичной рекурсивной схеме:

B = Apply (B1 · Apply (B2 · Apply (B3 ·... · Apply (BR1 · BR )))).

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

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

Пусть дана произвольная ROBDD B(f ), представляющая булеву функ цию f : {0, 1}n {0, 1} и построенная в соответствии с порядком означива ния переменных : x1 x2... xn (корень ROBDD помечен переменной x1 ). Рассмотрим произвольную подстановку на множестве {1,..., n} 1 2... n ( ) =, 1 2... n {1,..., n } = {1,..., n}. Будем говорить, что данная подстановка задает изменение исходного порядка на порядок, подразумевая, что столбец i подстановки с номером i, i {1,..., n}, имеющий вид, j {1,..., n}, j интерпретирует факт нахождения переменной xj в новом порядке на пози ции с номером i.

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

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

Колпаков А. В., Латыпов Р. Х. Приближенные алгоритмы минимиза ции двоичных диаграмм решений на основе линейных преобразований переменных // Автоматика и те лемеханика. 2004. Т. 6. С. 112–128.

Определение. Дана ROBDD B(f ), представляющая булеву функцию f : {0, 1}n {0, 1}, построенная в соответствии с заданным порядком :

x1 x2... xn. Требуется построить ROBDD B (f ), представляющую ту же самую функцию, в которой порядок означивания переменных из X есть, отличный от. Назовем данную проблему проблемой модификации ROBDD в соответствии с новым порядком. Ее частным случаем является проблема перестройки B(f ) в соответствии с произвольным порядком i таким, что i-тый столбец подстановки ( ) имеет вид, j = i.

j Эту проблему называем проблемой установки переменной xj на позицию с номером i.

Доказана следующая теорема (везде далее нумерация теорем соответ ствует их нумерации в тексте диссертации).

Теорема 2.1. Пусть ROBDD B(f ) представляет булеву функцию f от n переменных в соответствии с порядком : x1 xn.

x2...

Тогда для произвольных i, j {1,..., n} проблема установки переменной xj на позицию с номером i решается детерминированным образом за время O |B(f )|2.

Следствие теоремы 2.1. Пусть ROBDD B(f ) представляет булеву функцию f от n переменных в соответствии с порядком : x1 x xn. Тогда проблема модификации B(f ) в соответствии с произ...

вольным порядком сводится к l-кратному (l n) решению проблемы установки переменной на позицию с заданным номером.

Доказательство данного факта дает алгоритм модификации порядка в ROBDD, применяемый в дальнейшем в гибридном (SAT+ROBDD)-решателе.

В разделе 2.3 кратко описывается общая схема гибридного (SAT+RO BDD)-подхода к решению задач обращения полиномиально вычислимых дис кретных функций. В основе данного подхода лежит понятие ядра DPLL-выво да и возможности декомпозиционного разбиения решаемой задачи обраще ния на SAT- и ROBDD-части. Последующий процесс решения это сочета ние нехронологического DPLL-вывода на SAT-части с выводом на ROBDD.

Основные результаты данного раздела получены в неделимом соавторстве с научным руководителем диссертанта и приведены без доказательств.

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

Пусть B(f ) ROBDD-представление произвольной булевой функции f от переменных x1,..., xn. Каждой переменной xi, i {1,..., n}, и терми нальным вершинам 0, 1 поставим в соответствие множества значений данной переменной, задаваемых всевозможными путями в B(f ) из корня в соответствующую терминальную вершину. Данные множества обозначим че рез 0 (xi ), 1 (xi ).

Предположим, что в некоторой ROBDD B(f ) выполнены перечисленные ниже условия.

1) Для некоторой переменной xk X, X = {x1,..., xn }, любой путь из корня B(f ) в терминальную 1 обязательно проходит через некоторую вершину, помеченную переменной xk.

2) Справедливо 1 (xk ) = 1.

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

Определение. Определяемую условиями 1)-2) ситуацию далее называ ем ROBDD-следствием соответствующего значения для переменной xk.

Лемма 2.1. Выполнимость 1)-2) относительно некоторой переменной xk означает, что выполнено лишь одно из следующих условий:

1. для каждой вершины, помеченной xk, ее h-ребенком является терми нальная вершина 0 ;

2. для каждой вершины, помеченной xk, ее l-ребенком4 является терми нальная вершина 0.

Лемма 2.2. Процедура проверки возникновения ROBDD-следствий в ROBDD B(f ) требует детерминированного времени, ограниченного сверху величиной O (n · |B(f )|).

Далее изучается проблема отслеживания ROBDD-следствий в резуль тате подстановок в ROBDD конкретных значений некоторых переменных.

Такого рода подстановки осуществляются при помощи известной процеду ры Restrict, описанной Р. Брайантом. Предложен новый алгоритм, про веряющий возникновение ROBDD-следствий как результатов подстановок в ROBDD значений булевых переменных. С использованием лемм 2.1–2.2 дока зана следующая теорема.

Теорема 2.5. Пусть в ROBDD B(f ) подставляются значения пере менных xi1 = i1,..., xim = im, m n, ij {0, 1}, j {1,..., m}.

Тогда сложность детерминированной процедуры, осуществляющей данную подстановку и проверяющей наличие всевозможных ROBDD-следствий, ог раничена сверху величиной O (n · |B(f )|).

От high-child и low-child в английской нотации.

Процедура, о которой идет речь в теореме 2.5, получила название assign().

Справедливо следующее весьма важное в практическом отношении свойство.

Теорема 2.6. Если результатом применения процедуры assign() к B(f ) является ROBDD-следствие xk = k, k {0, 1}, для некоторой xk X, то подстановка в B(f ) xk = k не может привести к возникновению нового ROBDD-следствия, индуцированного данной подстановкой.

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

Еще одним полезным свойством гибридного вывода является возмож ность естественной организации на ROBDD т. н. отсроченных вычислений.

Рассмотрим следующие условия, которые определяют ситуацию, в некотором роде двойственную ситуации возникновения ROBDD-следствия.

i) Для некоторой переменной xq X в ROBDD B(f ) любой путь из корня в терминальную 0 обязательно проходит через некоторую вершину, помеченную переменной xq.

ii) Справедливо 0 (xq ) = 1.

Устанавливается справедливость следующей теоремы.

Теорема 2.7. Пусть B(f ) произвольная ROBDD и относительно некоторой переменной xq в B(f ) справедливы условия i) и ii). Тогда в RO BDD B(f ) невозможны ROBDD-следствия ни для каких переменных из множества X \ {xq }. Трудоемкость процедуры проверки условий i)–ii) огра ничена сверху величиной O (n · |B(f )|).

Данный результат позволяет сформировать механизмы отсроченных вы числений при подстановке выведенных значений некоторых переменных: если для текущей ROBDD B(f ) выполнены i)–ii) относительно xq, и из КНФ-части выведено значение некоторой переменной xk, k = q, нет смысла на данном эта пе подставлять соответствующее значение в B(f ) ничего нового выведено не будет. После присвоения или вывода из КНФ-части некоторого значения для xq целесообразно осуществить в B(f ) подстановку сразу всех накоплен ных к этому моменту значений переменных, а также вывод всех возможных ROBDD-следствий, используя для этого процедуру assign().

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

Некоторый алгоритм на основе DPLL действует в отношении КНФ C(f ), кодирующей задачу обращения функции f в некоторой точке. После пер вого рестарта вместо чистки базы конфликтных дизъюнктов, имеющей вид КНФ C, строится ROBDD-представление булевой функции, заданной фор мулой C. Дальнейший вывод идет как на исходной КНФ, так и на ROBDD, представляющей базу накопленных ограничений. При этом на ROBDD дей ствуют аналоги механизмов вывода, используемых в современных быстрых SAT-решателях на базе DPLL: аналог подстановки и правила единичного дизъюнкта реализован в виде процедуры assign(), описанной при доказатель стве теоремы 2.5;

аналогом CL-процедуры является применение алгоритма Р. Брайанта Apply к текущей ROBDD и новому ограничению-дизъюнкту;

отсроченные вычисления (аналог структуры watched literals ) организуются с учетом условий i)–ii) и результата теоремы 2.7.

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

В разделе 3.1 описывается архитектура ROBDD-решателя систем ло гических уравнений, в котором используются предложенные во второй гла ве эвристические алгоритмы реорганизации рассматриваемых систем по средством разбиения их на слои, а также специальный менеджер памяти, значительно повышающий эффективность процедур работы с оперативной памятью ЭВМ при построении ROBDD. Реализованный в соответствии с описанными принципами ROBDD-решатель был протестирован на задачах исследования некоторых дискретных автоматов, используемых в компьютер ной биологии. А именно, были решены задачи поиска неподвижных точек автоматных отображений, которые определяются графами, задающими ре гуляторные контуры дискретных моделей генных сетей5 (удавалось успешно решить соответствующие задачи для графов на 100 вершинах). Следует от метить, что эвристика разбиения на слои приводила к увеличению в разы эффективности процесса построения ROBDD-представлений характеристи ческих функций рассматриваемых систем логических уравнений.

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

ун-та. Приложение. 2005. Т. 14. С. 206–212.

Раздел 3.2 целиком посвящен описанию программного комплекса, в ко тором реализованы все описанные в работе алгоритмы. Данный программный комплекс представляет собой гибридный (SAT+ROBDD)-решатель, ориенти рованный на решение в РВС задач обращения полиномиально вычислимых дискретных функций. Главной мотивацией (SAT+ROBDD)-подхода к обра щению таких функций стало наблюдение о высокой степени ROBDD-сжа тия массивов конфликтных дизъюнктов, накапливаемых в процессе нехро нологического DPLL-вывода на КНФ, кодирующих соответствующие зада чи обращения. Это наблюдение стало результатом большого числа вычис лительных экспериментов. В задачах обращения некоторых криптографиче ских функций массивы конфликтных дизъюнктов объемами в сотни мегабайт сжимались (при помощи описанного выше ROBDD-решателя) в ROBDD, состоящие из десятков вершин и занимающих в памяти ЭВМ несколько кило байт. Такой малый размер ROBDD-представлений баз конфликтных ограни чений дает возможность эффективно обмениваться ими в РВС. Именно этот подход был реализован в построенном параллельном (SAT+ROBDD)-реша теле.

Основу параллельного решателя составляет последовательный гибрид ный (SAT+ROBDD)-решатель, названный hsat. Данный решатель функци онирует в соответствии со схемой, представленной на рисунке 1 (логический вывод ведется как на исходной КНФ, так и на ROBDD, представляющей базу накопленных ограничений-дизъюнктов).

Рис. 1. Схема работы гибридного (SAT+ROBDD)-решателя hsat Параллельный гибридный (SAT+ROBDD)-решатель получил название mhsat. Далее описаны основные принципы его работы. На k вычислитель ных ядрах запускается k версий решателя hsat, получающих на входе, вооб ще говоря, произвольную КНФ C. Все версии hsat стартуют с различными начальными порядками угадывания переменных. Процесс вывода является итерационным. Каждая итерация разбивается на два этапа. На первом эта пе все ядра работают независимо и на каждом происходит накопление кон фликтных дизъюнктов, причем база конфликтных ограничений имеет вид ROBDD (при этом используются все описанные выше механизмы гибрид ного (SAT+ROBDD)-вывода). На втором этапе все ядра обмениваются на копленными ограничениями (при этом возникает необходимость изменения в некоторых ROBDD порядка означивания переменных). Обмен происходит в соответствии со схемой, представленной на рисунке 2. После обмена ограниче ниями решатель снова переходит в режим независимой работы ядер (следую щая итерация). Работа продолжается до момента решения соответствующей SAT-задачи на некотором ядре.

Рис. 2. Схема обмена ограничениями в решателе mhsat (рассмотрен случай 8 ядер: P1–P8) Решатель mhsat был реализован с использованием стандарта MPI и про тестирован на задаче обращения дискретной функции, задающей порождение ключевого потока в системе шифрования A5/1. Следует отметить, что задача поиска выполняющего набора КНФ C(A5/1), непосредственно кодирующей криптоанализ A5/1, является очень сложной. Поэтому были рассмотрены ослабления этой задачи, а именно, рассматривались КНФ, из декомпозици онного семейства d = {C1 (A5/1),..., C2d (A5/1)}, полученного в результате подстановок в C(A5/1) всевозможных значений некоторых d булевых пере менных, выбираемых специальным образом. Именно такой подход использу ется при крупноблочном распараллеливании6 SAT-задач, кодирующих зада чи криптоанализа различных шифров (в том числе и A5/1).

В численных экспериментах рассматривались КНФ из декомпозицион ного семейства 20 = {C1 (A5/1),..., C220 (A5/1)} (d = 20). Решатель mhsat запускался на 4 ядрах процессора Intel R Xeon R E5345 с тактовой часто той 2,33 ГГц. Проводилось сравнение по эффективности mhsat, известного параллельного решателя MiraXT7, а также решателя dminisat6. Было сге нерировано 50 тестов (КНФ, выбираемые случайным образом из семейства 20 ). В среднем mhsat по эффективности на данном наборе тестов превзошел MiraXT в 2,88 раза, а dminisat в 5,12 раза.

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

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

основу метода составили новые ал горитмы логического вывода на ROBDD и ROBDD-аналоги основных механизмов, применяемых в нехронологическом DPLL-выводе;

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

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

Семенов А. А., Заикин О. С., Беспалов Д. В., Буров П. С., Хмельнов А. Е. Решение задач обраще ния дискретных функций на многопроцессорных вычислительных системах // Труды Четвертой Между народной конференции Параллельные вычисления и задачи управления (PACO’2008). Москва: 26– октября 2008. С. 152–176.

Schubert T., Lewis M., Becker B. PaMiraXT: Parallel SAT Solving with Threads and Message Passing // Journal on Satisability, Boolean Modeling and Computation. Special Issue on Parallel SAT Solving. 2009.

Vol. 6. Pp. 203–222.

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

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

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

Основные публикации по теме диссертации 1. Игнатьев А. С. Двоичные диаграммы решений в логических уравнениях и задачах обращения дискретных функций / А. Е. Хмельнов, А. С. Игнатьев, А. А. Семенов // Вестник НГУ.

Серия: Информационные технологии. 2009. Т. 7, № 4.

С. 36–52.

2. Игнатьев А. С. Использование двоичных диаграмм решений в задачах обращения дискретных функций / А. С. Игнатьев, А. А. Семенов, А. Е. Хмельнов // Вестник Томского гос. ун-та.

Серия: управление, вычислительная техника. 2009. № 1(6).

С. 115–129.

3. Игнатьев А. С. Алгоритмы работы с ROBDD как с базами булевых огра ничений / А. С. Игнатьев, А. А. Семенов // Прикладная дискретная мате матика. 2010. № 1. С. 86–104.

4. Игнатьев А. С. Решение систем логических уравнений с использованием BDD / А. С. Игнатьев, А. А. Семенов, А. Е. Хмельнов // Вестник Томского гос. ун-та. Приложение. 2006. № 17. С. 25–29.

5. Игнатьев А. С. Логические уравнения и двоичные диаграммы решений / А. А. Семенов, А. С. Игнатьев // Прикладные алгоритмы в дискретном анализе. Серия: Дискретный анализ и информатика. 2008. Т. 2.

С. 99–126. ISBN: 978-5-9624-0287-1.

6. Игнатьев А. С. Двоичные диаграммы решений в параллельных алгорит мах обращения дискретных функций / А. С. Игнатьев, А. А. Семенов, Д. В. Беспалов // Труды III Международной научной конференции ПАВТ’09. Нижний Новгород, ННГУ. 2009. С. 688–696. (ISBN:

978-5-696-03854-4).

7. Игнатьев А. С. Гибридный подход (SAT+ROBDD) в задачах крипто анализа поточных систем шифрования / А. С. Игнатьев, А. А. Семенов, Д. В. Беспалов, О. С. Заикин // Труды VIII школы-семинара с междуна родным участием Sibecrypt’09. Омск, ОмГТУ. 2009. № 1. С. 19–20.

Редакционно-издательский отдел Института динамики систем и теории управления СО РАН 664033, Иркутск, ул. Лермонтова, д. Подписано к печати dd.mm.year Формат бумаги 60 84 1/16, объем 1,2 п. л.

Заказ NN. Тираж 100 экз.

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

 

Похожие работы:





 
2013 www.netess.ru - «Бесплатная библиотека авторефератов кандидатских и докторских диссертаций»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.