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

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

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

МЕТОДЫ ОБРАЩЕНИЯ ДИСКРЕТНЫХ ФУНКЦИЙ С ПРИМЕНЕНИЕМ ДВОИЧНЫХ РЕШАЮЩИХ ДИАГРАММ

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

АВТОРЕФЕРАТ

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

Иркутск - 2010

004606127

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

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

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

Официальные оппоненты: доктор физико-математичеких наук,

профессор Перязев Николай Алексеевич

кандидат физико-математических наук, доцент Панкратова Ирина Анатольевна

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

Институт математики им. С. Л. Соболева СО РАН

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

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

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

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

канд. физ.-мат. наук, доцент

Антоник В. Г.

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

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

Задачи поиска решений логических уравнений дают пример проблем, чья аргументированная вычислительная сложность (в общей постановке они .ЫР-трудны) не является препятствием для появления новых методов и алгоритмов. Об актуальности данной проблематики свидетельствует хотя бы факт издания в Нидерландах специализированного журнала «^АТ» (см. http://jsat.ewi.tudelft.nl/), подавляющее большинство статей в котором посвящено ЭАТ-задачам (ЭАТ-задачами называются задачи поиска решений логических уравнений вида КНФ=1).

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

систем логических уравнений к уравнениям вида «КНФ=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-подходу. Решатели, базирующиеся на таких методах, могут использоваться при исследовании широкого класса дис-

1 Bryant II. Е. Graph-Based Algorithms for Boolean Function Manipulation // IEEE Transactions on Computers. 1986. Vol. 35, no S. Pp. 677-691.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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-задач. Заключительный раздел первой главы посвящен основам теории двоичных решающих диаграмм и их применению к логическим уравнениям и задачам обращения дискретных функций.

В этой же главе сформулирована основная проблема, исследуемая в диссертации и состоящая в следующем. Рассматривается натуральное семейство, образованное всюду определенными дискретными функциями вида /а : {0,1}" —> {0,1}*, вычислимыми за полиномиальное от п время. Проблемой обращения произвольной функции /„ из данного семейства в точке у называется следующая задача: по известному у G range fn и известному алгоритму вычисления /„ требуется найти такой х £ {0,1 }га, что fn(x) = у. Данная проблема может быть эффективно сведена к задаче поиска выполняющего набора КНФ С(/) над множеством булевых переменных X = {xi,..., £р(П)}, р(-) некоторый полином.

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

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

Рассматривается произвольная система (кратко обозначаемая через 5) логических уравнений вида

Здесь Li (х\,..., хп), j € {1,..., т}, формз'лы исчисления высказываний . (ИВ), X = {xi,..., а;«} — множество булевых переменных. Характеристической функцией системы S называется булева функция S$ : {0,1}" —> {0,1}, заданная формулой

Несложно понять, что по КОВВБ-представлению В{5в) функции 5$ проблема совместности системы 5, а также проблема поиска некоторого ее решения могут быть решены за линейное от ^(¿д)]- время (|В — число вершин в В (6б))- При построении В (5$) можно использовать различные эвристики организации порядка означивания переменных, а также строить декомпозиции исходной системы с целью разбиения процесса построения В (<5з) на независимые этапы. В диссертации для этих целей предложена новая эвристическая процедура разбиения системы 5 на подсистемы, называемые слоями. Пусть выбран некоторый порядок означивания переменных из X = {х\,...,я,,}, г : х^ -< х^ -< ... -< х(п_1 -< х,п, в соответствии с которым предполагается строить В (¿5). Число г £ {1,... , п} называем индексом переменной Ххг относительно выбранного порядка. Используя порядок т, разбиваем систему 5 на слои. Первый слой образован всеми уравнениями системы, в которые входит переменная х^. Второй слой образован всеми оставшимися уравнениями, содержащими переменную х^, которая имеет наименьший относительно т индекс по всем уравнениям, не входящим в первый слой. И так далее. Пусть К — число определяемых описанным образом слоев системы.

Li (xi,..., dyflj . . . (an,••• 1 •

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

Bj = Apply (Вь ■ Apply (Вк ■...■ Apply (Вк_, ■ Bjk))),

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

В = Apply (Bi • Apply (В2 ■ Apply (Вг ■... ■ Apply {BR-X ■ BR)))).

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

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

Пусть дана произвольная ROBDD B(f), представляющая булеву функцию / : {0,1}" —» {0,1} и построенная в соответствии с порядком означивания переменных т : хi -< Х2 -<■■■-< хп (корень ROBDD помечен переменной a;i). Рассмотрим произвольную подстановку на множестве {1,... , п}

, м /1 2 ... тЛ

а (т ->• т') = ,

\сц а2 ... anJ

{q'i, ... ,а„} = {1 ,...,n}. Будем говорить, что данная подстановка задает изменение исходного порядка т иа порядок г', подразумевая, что столбец

подстановки с номером г, i G {1,..., п}, имеющий вид ,j 6 {1,. • •, n},

интерпретирует факт нахождения переменной Xj в новом порядке г' на позиции с номером г.

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

3 Meinel Ch., Theobald Т. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications. Springer-Verlag, 1998; Колпаков А. В., Латыпов P. X. Приближенные алгоритмы минимизации двоичных диаграмм решений на основе линейных преобразований переменных // Автоматика и телемеханика. 2004. Т. 6. С. 112-128.

Определение. Дана ЯОВВО В(/), представляющая булеву функцию / : {0,1}" —> {0,1}, построенная в соответствии с заданным порядком т : Хг -< Хч < ... < хп. Требуется построить ЯОВПО В'(/), представляющую ту же самую функцию, в которой порядок означивания переменных из X есть т1, отличный от т. Назовел1 данную проблему проблемой модификации ИОВОВ в соответствии с новым порядком. Ее частным случаем является проблема перестройки В(/) е соответствии с произвольным порядком т'

таким, что г-тый столбец подстановки а (т —> т') имеет вид 3 Ф г-

Эту проблему называем проблемой установки переменной х^ на позицию с номером г.

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

Теорема 2.1. Пусть ЯОВОО В{}) представляет булеву функцию / от п переменных в соответствии с порядком, т : х\ ~< х^ -< ... -< хп. Тогда для произвольных г, ] € {1,...,я} проблема установки переменной ху на позицию с номером г решается детерминированным образом за время

Следствие теоремы 2.1. Пусть ROBDD B(f) представляет булеву функцию f от п переменных в соответствии с порядком т : х\ < х? < -<...-< хп. Тогда проблема модификации B(f) в соответствии с произвольным порядком г' сводится к 1-кратному (I < п) решению проблемы установки переменной на позицию с заданным номером.

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

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

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

Пусть B(f) — ROBDD-представление произвольной булевой функции / от переменных хх,...,хп. Каждой переменной Xi, i 6 {!,...,п], и терминальным вершинам «О», «1» поставим в соответствие множества значений данной переменной, задаваемых всевозможными путями в B(f) из корня в соответствующую терминальную вершину. Данные множества обозначим че-

рез Д%т,), Д1^)-

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

1) Для некоторой переменной Хк £ X, X = {ari,-..., хп}, любой путь ж из корня B(f) в терминальную «1» обязательно проходит через некоторую вершину, помеченную переменной х/¡.

2) Справедливо | А1 (а:^) j = 1.

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

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

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

1. для каэюдой вершины, помеченной Xk, ее h-ребенком является терминальная вершина «О»;

2. для каждой вершины, помеченной Хк, ее I-ребенком4 является терминальная вершина «О».

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

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

Теорема 2.5. Пусть в ROBDD i3(f) подставляются значения переменных

х^-аь,..., xim = aim, т<п, а^ £ {0,1}, j € {1,..., т}.

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

4 От thigh-child* и «low-child» в английской нотации-

Процедура, о которой идет речь и теореме 2-5, получила название assiynf). Справедливо следующее весьма важное в практическом отношении свойство.

Теорема 2.6. Если результатом применения процедуры assignf) к В(/) является ROBDD-следствие х* = аь a£ {0,1} . для некоторой Хк £ X, то подстановка в B(f) «Xk — ak» "e может привести к возникновению нового ROBDD-следствия, индуцированного данной подстановкой.

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

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

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

ii) Справедливо |А0(г9)| = 1.

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

Теорема 2.7. Пусть B(f) — произвольная ROBDD и относительно некоторой переменной xq в B(f) справедливы условия i) и it). Тогда в ROBDD B(f) невозможны ROBDD-следствия ни для каких переменных из множества Трудоемкость процедуры проверки условий iJ-iij огра-

ничена сверху величиной 0{п ■ |£?(/)|).

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

для xq целесообразно осуществить в B(f) подстановку сразу всех накопленных к этому моменту значений переменных, а также вывод всех возможных R.OBDD-следствий, используя для этого процедуру assignf).

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

Некоторый алгоритм на основе DPLL действует в отношении КНФ С(/), кодирующей задачу обращения функции / в некоторой точке. После первого рестарта вместо чистки базы конфликтных дизъюнктов, имеющей вид КНФ С', строится ROBDD-представление булевой функции, заданной формулой С'. Дальнейший вывод идет как на исходной КНФ, так и на ROBDD, представляющей базу накопленных ограничений. При этом на ROBDD действуют аналоги механизмов вывода, используемых в современных быстрых SAT-решателях на базе DPLL: аналог подстановки и правила единичного дизъюнкта реализован в виде процедуры assignf), описанной при доказательстве теоремы 2.5; аналогом CL-процедуры является применение алгоритма Р. Брайанта «Apply» к текущей ROBDD и новому ограничению-дизъюнкту; отсроченные вычисления (аналог структуры «watched literals») организуются с учетом условий i)-ii) и результата теоремы 2.7.

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

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

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

Раздел 3.2 целиком посвящен описанию программного комплекса, в котором реализованы все описанные в работе алгоритмы. Данный программный комплекс представляет собой гибридный (БАТ+КОВВВ)-решатель, ориентированный на решение в РВС задач обращения полиномиально вычислимых дискретных функций. Главной мотивацией (8АТ-г1ЮВОВ)-подхода к обращению таких функций стало наблюдение о высокой степени «ЕОВВБ-сжа-тия» массивов конфликтных дизъюнктов, накапливаемых в процессе нехронологического ЭРЬЬ-вывода на КНФ, кодирующих соответствующие задачи обращения. Это наблюдение стало результатом большого числа вычислительных экспериментов. В задачах обращения некоторых криптографических функций массивы конфликтных дизъюнктов объемами в сотни мегабайт «сжимались» (при помощи описанного выше ТЮВОВ-решателя) в ИОВОБ, состоящие из десятков вершин и занимающих в памяти ЭВМ несколько килобайт. Такой малый размер КОВВО-представлений баз конфликтных ограничений дает возможность эффективно обмениваться ими в РВС. Именно этот подход был реализован в построенном параллельном (8АТ+ЯОВОВ)-реша-теле.

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

1

ROBDD-вывод на

Рис. 1. Схема работы гибридного (ЗАТн-НОВОВ)-решателя hsat

Параллельный гибридный (SAT ! ШВБО)-решатель получил название «mhsat». Далее описаны основные принципы его работы. На к вычислитель-

пых ядрах запускается к версий решателя Ьяа^ получающих на входе, вообще говоря, произвольную КНФ С. Все версии 1ша1 стартуют с различными начальными порядками угадывания переменных. Процесс вывода является итерационным. Каждая итерация разбивается на два этапа. На первом этапе все ядра работают независимо и на каждом происходит накопление конфликтных дизъюнктов, причем база конфликтных ограничений имеет вид КОВБО (при этом используются все описанные выше механизмы гибридного (8АТ+КОВБО)-вывода). На втором этапе все ядра обмениваются накопленными ограничениями (при этом возникает необходимость изменения в некоторых КОВБО порядка означивания переменных). Обмен происходит в соответствии со схемой, представленной на рисунке 2. После обмена ограничениями решатель снова переходит в режим независимой работы ядер (следующая итерация). Работа продолжается до момента решения соответствующей БАТ-задачи на некотором ядре.

Рис. 2. Схема обмена ограничениями б решателе тЬьа! (рассмотрен случай 8 ядер: Р1-Р8)

Решатель mhsat был реализован с использованием стандарта MPI и протестирован на задаче обращения дискретной функции, задающей порождение ключевого потока в системе шифрования А5/1. Следует отметить, что задача поиска выполняющего набора КНФ С(А5/1), непосредственно кодирующей криптоанализ А5/1, является очень сложной. Поэтому были рассмотрены ослабления этой задачи, а именно, рассматривались КНФ, из декомпозиционного семейства А^ - {С[(А5/1),..., А5/1)}, полученного в результате подстановок в С(А5/1) всевозможных значений некоторых d булевых переменных, выбираемых специальным образом. Именно такой подход используется при крупноблочном распараллеливании6 SAT-задач, кодирующих задачи криптоанализа различных шифров (в том числе и А5,< 1).

В численных экспериментах рассматривались КНФ из декомпозиционного семейства Д20 = {С{(А5/1),... ,С22о(А5/1)} (d = 20). Решатель mhsat запускался па 4 ядрах процессора Intel® Xeon® Е5345 с тактовой частотой 2,33 ГГц. Проводилось сравнение по эффективности mhsat, известного параллельного решателя MiraXT7, а также решателя dmmisat6. Было сгенерировано 50 тестов (КНФ, выбираемые случайным образом из семейства Д20). В среднем mhsat по эффективности на данном наборе тестов превзошел MiraXT в 2,88 раза, a dminisat —в 5,12 раза.

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

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

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

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

7 Schubert Т., Lewis M., Becker В. PaMiraXT: Parallel SAT Solving with Threads and Message Passing / Journal on Satisfiability. Boolean Modeling and Computation. Special Issue on Parallel SAT Solving. 2009.

Vol. (i. Pp. 203-222.

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

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

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

Основные публикации по теме диссертации

1. Игнатьев А. С. Двоичные диаграммы решений в логических уравнениях и задачах обращения дискретных функций / А. Е. Хмельнов, А. С. Игнатьев, A.A. Семенов // Вестник НГУ. Серия: Информационные технологии. — 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 школы-семинара с международным участием Sibccrypt'09. Омск, ОмГТУ. - 2009. - С. 19-20.

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

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

Введение

Глава 1. Дискретные функции, логические уравнения и двоичные диаграммы решений

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

1.2. SAT-подход к задачам обращения дискретных функций (краткое описание).

1.2.1. Основа SAT-подхода.

1.2.2. Основные алгоритмы решения SAT-задач.

1.3. Двоичные решающие диаграммы.

1.3.1. Базовые понятия.

1.3.2. Основные алгоритмы работы с BDD.

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

2.1. Алгоритмика ROBDD-подхода к решению систем логических уравнений

2.1.1. Специальные представления формул ИВ.

2.1.2. Разбиение системы на слои и использование шаблонов

2.2. Процедуры изменения порядка означивания переменных в ROBDD.

2.3. Основы гибридного (SAT+ROBDD) подхода к задачам обращения дискретных функций.

2.4. Логический вывод на ROBDD (основные алгоритмы)

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

3.1.1. Базовые структуры данных.

3.1.2. Организация работы с памятью при работе ROBDD

3.1.3. Применение ROBDD-решателя логических уравнений к исследованию дискретно-автоматных моделей генных сетей

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

3.2.1. Реализация и тестирование последовательного гибридного (8АТ+К0ВББ)-решателя.

3.2.2. Реализация и тестирование параллельного гибридного (8АТ+КОВБВ)-решателя, функционирующего в MPI-среде.

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

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

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

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

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

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

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

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

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

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

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

3. Программно реализовать гибридный (SAT-f-ROBDD)-peiiiaTejib логических уравнений, ориентированный на задачи обращения полиномиально вычислимых дискретных функций; разработать параллельные гибридные (ЗАТЧ-^ОВВВ)-алгоритмы решения логических уравнений и обращения дискретных функций; программно реализовать разработанные алгоритмы с использованием стандарта MPI (Message Passing Interface); интегрировать все разработанные алгоритмы в программный комплекс.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В разделе 3.2 описывается программный комплекс, основанный на концепции гибридного (SAT+ROBDD)-noflxofla к обращению полиномиально вычислимых дискретных функций. В данном комплексе были реализованы все алгоритмы описанные во второй главе. Основной предпосылкой эффективности гибридного (SAT+ROBDD)-noflxofla является наблюдаемый в экспериментах эффект «ROBDD-сжатия» баз ограничений-дизъюнктов, накапливаемых в процессе нехронологического DPLL-вывода. Разработанный комплекс был реализован с использованием стандарта MPI и функционирует в распределенных вычислительных средах. Его принципиальным отличием от современных решателей SAT-задач, использующих межпроцессорные взаимодействия, является технология обмена независимо накапливаемыми булевыми ограничениями, представляемыми в виде ROBDD. Заключительный пункт данного раздела содержит результаты численных экспериментов, в которых разработанный программный комплекс был протестирован на задачах обращения некоторых криптографических функций.

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

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

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

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

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

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

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

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

Заключение

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

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

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

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

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

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

1. Bryant R. E. Graph-Based Algorithms for Boolean Function Manipulation / R. E. Bryant // 1.EE Transactions on Computers. — 1986. — Vol. 35, no. 8. - Pp. 677-691.

2. Мендельсон Э. Введение в математическую логику / Э. Мендельсон.

3. Москва: «Наука», 1971. — С. 320.

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

5. Нигматуллип Р. Г. Сложность булевых функций / Р. Г. Нигматуллин.

6. Москва: «Наука», 1991. — С. 240.

7. Сэвидж Дж. Э. Сложность вычислений / Дж. Э. Сэвидж. — Москва: «Факториал», 1998. С. 368.

8. Закревский А. Д. Логические уравнения / А. Д. Закревский. — Минск: Наука и техника, 1975. — С. 94.

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

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

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

12. Stockmeyer L. Classifying of computational complexity of problems / L. Stockmeyer // The Journal of Symbolic Logic. — 1987. — Vol. 52, no. 1. Pp. 1-43.

13. Стокмейер Л. Классификация вычислительной сложности проблем / Л. Стокмейер // Кибернетический сборник. Новая серия. — 1989. — Т. 26. С. 20-83.

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

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

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

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

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

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

20. Кук С. А. Сложность процедур вывода теорем / С. А. Кук // Кибернетический сборник. Новая серия. — 1975. — Т. 12. — С. 5-15.

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

22. Buchberger В. Grobner-Bases: An Algorithmic Method in Polynomial Ideal Theory / B. Buchberger // Multidimensional Systems Theory. — 1985. Vol. 6. - Pp. 184-232.

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

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

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

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

27. Btittner W. Embedding Boolean expressions into logic programming / W. Biittner, H. Simonis // Journal of Symbolic Computation. — 1987.1. Vol. 4. Pp. 191-205.

28. Brown F. M. Boolean Reasoning: The Logic Of Boolean Equations /

29. F. M. Brown. — Dover Publications, 2003. — P. 304.

30. Meinel Ch. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications / Ch. Meinel, T. Theobald. — Springer-Ver-lag, 1998.

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

32. Tseitin G. On the complexity of derivation in propositional calculus /

33. G. Tseitin // Studies in Constructive Mathematics and Mathematical Logic. — 1968. Vol. 2. - Pp. 234-259.

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

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

36. SATLive! Электронный ресурс]. — Режим доступа: http://www. satlive. org/.

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

38. Drechsler R. Formal Verification of Circuits / R. Drechsler. — Kluwer Academic Publishers, 2000.

39. Advanced Formal Verification / Ed. by R. Drechsler. — Kluwer Academic Publishers, 2004.

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

41. Robinson J. A. A Machine-Oriented Logic Based on the Resolution Principle / J. A. Robinson // Journal of the ACM (JACM). 1965. - Vol. 12, no. 1. - Pp. 23-41.

42. Робинсон Дж. А. Машинно-ориентированная логика, основанная на принципе резолюций / Дж. А. Робинсон // Кибернетический сборник. Новая серия. 1970. - Vol. 7. — Pp. 194-217.

43. Riazanov A. The Design and Implementation of Vampire / A. Riazanov, A. Voronkov // AI Communications. — 2002. — Vol. 15, no. 2-3. — Pp. 91-110.

44. McCune W. Otter: The CADE-13 Competition Incarnations / W. Mc-Cune, L. Wos // Journal of Automated Reasoning. — 1997. — Vol. 18, no. 2. — Pp. 211-220.

45. Kalman J. A. Automated reasoning with Otter / J. A. Kalman. — Princeton, N. J.: Rinton Press, 2001.

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

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

48. Братко И. Алгоритмы искусственного интеллекта на языке PROLOG / И. Братко. «Вильяме», 2004. - С. 640.

49. Algorithms for the satisfiability (SAT) problem: A Survey / J. Gu, P. Pur-dom, J. Franco, B. W. Wall // DIMACS Series in Discrete Mathematics and Theoretical Computer Science. — 1997. — Vol. 35, no. 4. — Pp. 19-152.

50. Gu J. Local search for satisfiability (SAT) problem / J. Gu // IEEE Transactions on Systems, Man, and Cybernetics. — 1993. — Vol. 23, no. 4. Pp. 1108-1129.

51. Gu J. Global optimization for satisfiability (SAT) problem / J. Gu // IEEE Transactions on Knowledge and Data Engineering. — 1994. — Vol. 6, no. 3. Pp. 361-381.

52. Gu J. Optimization Algorithms for the Satisfiability (SAT) Problem / J. Gu // Advances in Optimization and Approximation / Ed. by D.-Z. Du; Kluwer Academic Publishers. — 1994. — Pp. 72-154.

53. Davis M. A machine program for theorem-proving / M. Davis, G. Loge-mann, D. Loveland // Communications of the ACM. — 1962. — Vol. 5, no. 7. Pp. 394-397.

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

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

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

57. Een N. An Extensible SAT-solver extended version 1.2] / N. Een, N. Sorensson. 2003.

58. Bohm M. A Fast Parallel SAT-Solver — Efficient Workload Balancing / M. Bohm, E. Speckenmeyer // Annals of Mathematics and Artificial Intelligence. 1996. - Vol. 17, no. 3-4. - Pp. 381-400.

59. Chrabakh VV. GridSAT: A Chaff-based Distributed SAT Solver for the Grid / W. Chrabakh, R. Wolski // ACM/IEEE Supercomputing Conference. — 2003.

60. Jurkowiak B. Parallelizing Satz using Dynamic Workload Balancing / B. Jurkowiak, C.M. Li, G. Utard // LICS 2001 Workshop on Theory and Applications of Satisfiability Testing. — 2001. — Pp. 205-211.

61. Zhang H. PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems / H. Zhang, M. Bonacina, J. Hsiang // Journal of Symbolic Computation. — 1996. — Vol. 21, no. 4. Pp. 543-560.

62. C. Sinz W. Blochinger. PaSAT Parallel SAT-Checking with Lemma Exchange: Implementation and Applications / W. Blochinger C. Sinz, W. Ktichlin // LICS 2001 Workshop on Theory and Applications of Satisfiability Testing. - 2001.

63. Feldman Y. Parallel Multithreaded Satisfiability Solver: Design and Implementation / Y. Feldman, N. Dershowitz, Z. Hanna // Electronic Notes in Theoretical Computer Science. — 2005. — Vol. 128, no. 3. — Pp. 75-90.

64. Schubert T. PaMira a Parallel SAT Solver with Knowledge Sharing / T. Schubert, M. Lewis, B. Becker // 6th International Workshop on Microprocessor Test and Verification. — 2005. — Pp. 29-34.

65. Gil L. PMSat: a parallel version of MiniSAT / L. Gil, P. Flores, L. M. Sil-veira // Journal on Satisfiability, Boolean Modeling and Computation. — 2008. Vol. 6. - Pp. 71-98.

66. Schubert T. PaMiraXT: Parallel SAT Solving with Threads and Message Passing / T. Schubert, M. Lewis, B. Becker // Journal on Satisfiability, Boolean Modeling and Computation. Special Issue on Parallel SAT Solving. 2009. - Vol. 6. - Pp. 203-222.

67. Davis M. A Computing Procedure for Quantification Theory / M. Davis, H. Putnam // Journal of the ACM (JACM). 1960. - Vol. 7, no. 3. -Pp. 201-215.

68. Haken A. The intractability of resolution / A. Haken // Theoretical Computer Science. — 1985. — Vol. 39. Pp. 297-308.

69. Хакен А. Труднорешаемость резолюций / А. Хакеи // Кибернетический сборник. Новая серия. — 1991. — Vol. 28. — Pp. 179-194.

70. Ben-Sasson Е. Near Optimal Separation on Tree-like and General Resolution / E. Ben-Sasson, R. Impagliazzo, A. Wigderson // Combinatorica. 2004. - Pp. 585-603.

71. An exponential separation between regular and general resolution / M. Aleklmovich, J. Johannsen, T. Pitassi, A. Urquhart //In 34th Annual ACM Symposium on Theory of Computing. — 2002. — Pp. 448-456.

72. Jeroslaw R. G. Solving propositional satisfiability problems / R. G. Jeroslaw, J. Wang // Annals of Mathematics and Artificial Intelligence. 1990. - Vol. 1. - Pp. 167-187.

73. Chaff: engineering an efficient SAT solver / M. W. Moskewicz, C. F. Madi-gan, Y. Zhao et al. // Proceedings of the 38th annual Design Automation Conference. 2001. - Pp. 530-535.

74. Beame P. Understanding the power of clause learning / P. Beame,

75. H. Kautz, A. Sabharwal // Proc. Of 18th Intern. Joint Conf. on Artificial Intelligence (IJCAI). — 2003. Pp. 1194-1201.

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

77. Zhang Н. SATO: An efficient propositional prover / H. Zhang // Proceedings of International Conference on Automated deduction. — 1997.- Pp. 272-275.

78. Lynce I. Efficient data structures for backtrack search SAT solvers /

79. Lynce, J. P. Marques-Silva // 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT'02). — 2002.

80. Lee C. Y. Representation of Switching Circuits by Binary-Decision Programs / C. Y. Lee // Bell Systems Technical Journal. — 1959. — Vol. 38.- Pp. 985-999.

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

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

83. Shilov N. V. How to find a coin: propositional program logics made easy / N. V. Shilov, K. Yi // Current Trends in Theor. Comput. Sci., World Scientific. 2004. - Vol. 2. — Pp. 181-213.

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

85. Семичева Н. JI. Нахождение бесповторных представлений недоопре-деленных частичных булевых функций / Н. JI. Семичева // серия «Дискретная математика и информатика». — 2008. — Т. 19. — С. 35.

86. Зубков О. В. Оценки числа бесповторных булевых функций в бинарных базисах / О. В. Зубков // серия «Дискретная математика и информатика». 2002. - Т. 15. - С. 34.

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

88. Игнатьев А. С. Использование двоичных диаграмм решений в задачах обращения дискретных функций / А. С. Игнатьев, А. А. Семенов, А. Е. Хмельнов // Вестник Томского гос. ун-та. Серия: управление, вычислительная техника. — 2009. — № 1(6). — С. 115-129.

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

90. Andersen Н. R. An Introduction to Binary Decision Diagrams. Lecture Notes / H. R. Andersen. — Copenhagen: Technical University of Denmark, 1997.

91. Valiant L. G. The complexity of computing the permanent /

92. G. Valiant // Theoretical Computer Science. — 1979. — Vol. 8. — Pp. 189-202.

93. Valiant L. G. The complexity of enumeration and reliability problems / L. G. Valiant // SIAM Journal on Computing. — 1979. — Vol. 8. — Pp. 410-421.

94. Семенов А. А. Декомпозиционные представления логических уравнений в задачах обращения дискретных функций / А. А. Семенов // Известия РАН. Теория и системы управления. — 2009. — N2 5. — С. 47-61.

95. Левитин А. Алгоритмы. Введение в разработку и анализ / А. Левитин. — «Вильяме», 2006. — С. 576.

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

97. Хмельнов А. Е. Двоичные диаграммы решений в логических уравнениях и задачах обращения дискретных функций / А. Е. Хмельнов, А. С. Игнатьев, А. А. Семенов // Вестник НГУ. Серия: Информационные технологии. — 2009. — Т. 7, № 4. С. 36-52.

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

99. Efficient conflict driven learning in a boolean satisfiability solver / L. Zhang, C. Madigan, M. Moskewicz, S. Malik // Proc. Intern. Conf. on Computer Aided Design (ICCAD). 2001. - Pp. 279-285.

100. Кормен Т. Алгоритмы: построение и анализ / Т. Кормен, Ч. Лейзер-сон, Р. Ривест. — Москва: МЦНМО: БИНОМ, 2004. С. 960.

101. Wikipedia. Электронный ресурс]. — Режим доступа: http://en. wikipedia.org/wiki/Thrash(computerscience).

102. Fortune S. J. A sweepline algorithm for Voronoi diagrams / S. J. Fortune // Algorithmica. — 1987. — Pp. 153-174.

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

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

105. Евдокимов А. А. Символьные алгоритмы в исследовании дискретных моделей некоторых классов генных сетей / А. А. Евдокимов, С. Е. Ко-чемазов, А. А. Семенов // Препринт. Издательство ИДСТУ СО РАН.- 2010.

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

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

108. MiniSat. Электронный ресурс]. — Режим доступа: http: //minisat. se/MiniSat.html.

109. Biryukov A. Real Time Cryptanalysis of A5/1 on a PC / A. Biryukov, A. Shamir, D. Wagner // Fast Software Encryption Workshop. — 2000.- Pp. 1-18.

110. Menezes A. Handbook of Applied Cryptography / A. Menezes, P. van Oor-shot, S. Vanstone. CRC Press, 1996. — P. 657.

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

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

113. JSAT Volume 6. Электронный ресурс]. — Режим доступа: http:// jsat.ewi.tudelft.nl/content/volume6-contents.html.

114. SAT-Race 2008. Электронный ресурс]. — Режим доступа: http:// baldur.iti.uka.de/sat-race-2008/.

115. Hamadi Y. ManySAT: a Parallel SAT Solver / Y. Hamadi, S. Jabbour, L. Sais // Journal on Satisfiability, Boolean Modeling and Computation. Special Issue on Parallel SAT " " 009. Vol. 6. — Pp. 245-262.