Содержание к диссертации
Введение
Глава 1. SAT-задачи и основные технологии, используемые при их решении 12
1.1. Постановка SAT-задач. Сведение задач обращения дискретных функций к SAT-задачам 12
1.2. Методы и алгоритмы решения SAT-задач 20
1.3. Области применения SAT-задач 33
Глава 2. Технология крупноблочного параллелизма в решении SAT- задач 39
2.1. Методы параллельного решения SAT-задач 39
2.2. Крупноблочный параллелизм в SAT-задачах 41
2.3. Прогнозирование времени параллельного решения SAT-задач 46
2.4. Схемы формирования декомпозиционных множеств 54
Глава 3. Пакет прикладных программ D-SAT и вычислительные эксперименты 65
3.1. Описание пакета прикладных программ D-SAT 65
3.1.1. Библиотека программ пакета D-SAT 68
3.1.2. Режимы работы пакета D-SAT 70
3.1.3. Дополнительные аспекты пакета D-SAT 74
3.2. Параллельный логический криптоанализ некоторых генераторов ключевого потока 82
3.2.1. Особенности пропозиционального кодирования генераторов ключевого потока 82
3.2.1. Криптоанализ генератора Гиффорда 86
3.2.2. Криптоанализ суммирующего генератора 89
3.2.3. Криптоанализ порогового генератора 92
3.2.4. Прогнозирование трудоемкости параллельного логического криптоанализа генератора А5/1 96
Заключение 102
Список использованной литературы 103
Приложение 1. Подход к формированию истинно случайных последовательностей 114
- Постановка SAT-задач. Сведение задач обращения дискретных функций к SAT-задачам
- Методы и алгоритмы решения SAT-задач
- Методы параллельного решения SAT-задач
- Библиотека программ пакета D-SAT
Введение к работе
Актуальность работы
Многие значимые в практическом отношении проблемы, связанные с управлением и обработкой информации в дискретных системах, допускают эффективные сводимости к задачам поиска решений логических уравнений. Сказанное касается проблем синтеза и верификации в микроэлектронике, целого ряда вопросов теоретического программирования, задач обращения дискретных функций, задач управления коммуникационными протоколами и многих других. Один из наиболее важных классов логических уравнений образован уравнениями вида «КНФ =1» (КНФ - конъюнктивная нормальная форма). Задачи поиска решений данного класса уравнений относятся к так называемым «SAT-задачам». Для решения SAT-задач используются специальные программные комплексы, называемые SAT-решателями. В построении SAT-решателей в последние годы отмечен реальный прогресс.
Высокая вычислительная сложность SAT-задач аргументирует использование для их решения параллельных вычислений. С этой позиции SAT-задачи могут исследоваться по двум направлениям.
Первое направление основывается на концепции мелкозернистого параллелизма. В этом случае распараллеливание осуществляется на уровне базового алгоритма SAT-решателя (SAT-решатели с параллельной вычислительной архитектурой). Однако современные SAT-решатели являются довольно сложными в структурном смысле программами, в связи с чем реализация данного подхода трудна в техническом отношении. Кроме этого, мелкозернистый параллелизм зачастую характеризуется невысокой масштабируемостью.
В основе второго направления лежит концепция крупноблочного параллелизма. В этом случае осуществляется декомпозиция исходной SAT-задачи на семейство подзадач, каждая из которых обрабатывается SAT-
решателем на отдельном вычислительном узле параллельной вычислительной системы. При этом параллельная вычислительная система свободна от ряда ограничений, присущих мелкозернистому параллелизму. Кроме этого, крупноблочный подход, как правило, характеризуется высокой масштабируемостью. Крупноблочный параллелизм предпочтителен в решении SAT-задач, в которых размерность пространства полного перебора существенно меньше числа булевых переменных, фигурирующих в КНФ. Речь идет, прежде всего, о SAT-задачах, к которым сводятся задачи обращения дискретных функций из класса, имеющего пересечения с многочисленными областями кибернетики.
Сказанное означает, что проблема создания эффективных технологий решения SAT-задач посредством их крупноблочного распараллеливания является актуальной.
Цель работы и задачи исследования
Целью диссертационной работы является разработка и практическая реализация технологии крупноблочного распараллеливания SAT-задач.
Для достижения указанной цели ставятся и решаются следующие основные задачи.
1. Разработка и исследование различных стратегий построения
декомпозиционных представлений SAT-задач.
2. Разработка и алгоритмическая реализация процедуры
прогнозирования трудоемкости параллельного решения SAT-задач.
3. Программная реализация технологии крупноблочного
распараллеливания SAT-задач в форме пакета прикладных программ (ППП).
4. Решение с помощью разработанного ППП SAT-задач, кодирующих
задачи обращения ряда дискретных функций, используемых в криптографии.
Методы исследования
Теоретические исследования используют аппарат теории множеств, дискретной математики, теории вычислительной сложности, параллельных вычислений, а экспериментальные - инструментальные и программные средства решения задач в параллельных вычислительных системах.
Научная новизна
Новыми являются все основные результаты, полученные в диссертации, в том числе:
- общая схема крупноблочного распараллеливания SAT-задач;
- процедура прогнозирования трудоемкости параллельного решения
SAT-задач;
- оценка сложности процедуры прогнозирования трудоемкости
параллельного решения SAT-задач;
- разработка ППП для реализации параллельной технологии решения
SAT-задач;
- параллельное решение с помощью разработанного ППП
вычислительно сложных SAT-задач, кодирующих задачи обращения
некоторых дискретных функций, используемых в криптографии.
При решении поставленных задач были получены перечисленные ниже вспомогательные результаты, представляющие самостоятельный интерес. Введено понятие декомпозиционного множества; введено понятие схемы формирования семейств декомпозиционных множеств (далее «схема формирования»); введена классификация схем формирований; разработаны схемы формирования, ориентированные на структуру SAT-задач, кодирующих задачи обращения некоторых дискретных функций; реализована процедура оптимизированной рассылки SAT-задач, снижающая транспортные расходы в параллельных вычислительных системах.
Теоретическая и практическая значимость работы
Теоретическая значимость работы аргументируется возможностью прямого переноса ее базовых концепций на задачи дискретной оптимизации с двоичными данными. Разработанные в диссертации методы и алгоритмы могут применяться для решения широкого класса практически важных задач, допускающих эффективную сводимость к SAT-задачам.
Достоверность результатов
Достоверность полученных в работе теоретических результатов обеспечивается строгостью производимых математических построений. Корректность и эффективность практической реализации подтверждается результатами вычислительных экспериментов.
Основные результаты, выносимые на защиту
1. Параллельная технология решения SAT-задач, включающая общую
схему крупноблочного распараллеливания SAT-задач.
2. Разработка и анализ различных схем формирования
декомпозиционных представлений SAT-задач.
3. Процедура прогнозирования трудоемкости параллельного решения
SAT-задач; оценка сложности данной процедуры.
4. Разработка ППП для практической реализации предложенной
параллельной технологии решения SAT-задач.
5. Параллельное решение с помощью разработанного ППП
вычислительно сложных SAT-задач, кодирующих задачи обращения
некоторых дискретных функций, используемых в криптографии.
Работа состоит из введения, 3-х глав, заключения и списка литературы.
В первой главе описывается SAT-подход к решению задач обращения дискретных функций. Приведен обзор основных компонентов архитектуры
современных SAT-решателей. Описана концепция логического криптоанализа.
В разделе 1.1 рассматривается специальный класс з, образованный всеми всюду определенными алгоритмически вычислимыми (за полиномиальное от длины входа время) семействами дискретных функций. Задача обращения дискретной функции семейства 3 ставится следующим образом: по известному образу найти хотя бы один прообраз. Проблемы обращения функций произвольного семейства из класса 3 допускают эффективную сводимость к проблемам поиска решений логических уравнений вида «КНФ=1», где КНФ - это конъюнктивная нормальная форма над некоторым множеством булевых переменных. Задачи поиска решений таких уравнений называются SAT-задачами.
В разделе 1.2 рассмотрены основные компоненты архитектуры современных эффективных SAT-решателей (программных комплексов, решающих SAT-задачи), основанных на алгоритме DPLL. Приведен обзор следующих базовых технологий, используемых в такого рода SAT-решателях: бэктрекинг, нехронологический бэктрекинг, правило единичного дизъюнкта, ВСР-стратегия, процедура «Clause Learning», процедуры чистки базы ограничений, рестарты.
В разделе 1.3 описывается концепция логического криптоанализа (криптоанализ, рассматриваемый как SAT-задача). В отношении генераторов ключевого потока приводится постановка логического криптоанализа как задачи обращения дискретных функция из класса 3.
Во второй главе описана параллельная технология решения SAT-задач. Предложены различные виды декомпозиционных представлений и описана процедура прогнозирования трудоемкости параллельного решения SAT-задач.
В разделе 2.1 кратко охарактеризованы особенности мелкозернистого и
крупноблочного подходов к параллельному решению SAT-задач.
В разделе 2.2 описана методика крупноблочного распараллеливания SAT-задач. Общая идея данной методики состоит в следующем.
Рассматривается произвольная КНФ (называемая далее исходной) над множеством булевых переменных X. Декомпозиционным множеством называется некоторое подмножество X' множества X. Декомпозиционному множеству X' ставится в соответствие множество Y{X')={Yx,...,Yk), состоящее из k = 2d различных двоичных векторов, каждый из которых является вектором значений переменных из X'. Декомпозиционным семейством называется множество КНФ, полученных подстановками в исходную КНФ векторов из y(X'). Всякому набору, выполняющему исходную КНФ, соответствует набор, выполняющий некоторую КНФ из декомпозиционного семейства. Наоборот, произвольному набору, выполняющему некоторую КНФ из декомпозиционного семейства, соответствует единственный набор, выполняющий исходную КНФ. Таким образом, SAT-задача относительно исходной КНФ сводится к решению SAT-задач для КНФ из декомпозиционного семейства.
В разделе 2.3 предложена процедура прогнозирования трудоемкости параллельного решения SAT-задач при их крупноблочном распараллеливании.
Предположим, что зафиксировано некоторое декомпозиционное множество X'. Представляет интерес «улучшение» X', то есть построение такого подмножества X', использование которого в качестве декомпозиционного множества делают декомпозицию более эффективной, чем на основе X'.
Предлагается специальная процедура статистического прогнозирования, предназначенная для «улучшения» декомпозиционного множества. Представление о трудоемкости соответствующего параллельного
вычисления можно составить на основе знания среднего времени решения SAT-задач для серии КНФ, выбранных случайным образом из декомпозиционного множества. Введена специальная прогнозная функция и задача выбора оптимального (по прогнозу) декомпозиционного множества решается через задачу оптимизации данной функции.
В разделе 2.4 предлагается методика построения декомпозиционных множеств. Основой данной методики является понятие схемы формирования декомпозиционного множества (далее «схема формирования»). Схема формирования - это алгоритм построения декомпозиционных множеств заданной мощности. Здесь же предлагается совмещение технологии статистического прогнозирования с использованием различных схем формирования. При этом каждой схеме формирования ставится в соответствие прогноз трудоемкости параллельного вычисления, после чего выбирается схема формирования и соответствующая декомпозиция, дающие наилучшие прогнозные значения.
В третьей главе приведено описание пакета прикладных программ (ППП) D-SAT1 (созданного для реализации параллельной технологии, предложенной во второй главе), а также результаты вычислительных экспериментов.
В разделе 3.1 описаны архитектура и основные функции ППП D-SAT.
ППП D-SAT функционирует в РВС под управлением инструментального комплекса Distributed Computing system of Modular Programming (DISCOMP2). Библиотека программ ППП D-SAT включает модуль расщепления, модуль SAT-решателя, модуль прогнозирования, модуль сравнения, аналитический модуль и транспортный модуль.
1 Заикин О.С. Пакет прикладных программ Distributed-SAT: Свидетельство об официальной регистрации
программы для ЭВМ № 2008610423. — М.: Федеральная служба по интеллектуальной собственности,
патентам и товарным знакам, 2008.
2 Разработчик Сидоров И.А., ИДСТУ СО РАН
В разделе 3.2 на серии численных экспериментов продемонстрировано успешное использование ШШ D-SAT в решении задач логического криптоанализа ряда генераторов, последовательный логический криптоанализ которых не дал приемлемых результатов. Так, с помощью 111111 D-SAT был осуществлен успешный параллельной логический криптоанализ генератора Гиффорда, а также суммирующего и порогового генераторов.
Внедрение результатов исследований
Результаты диссертации внедрены:
в разработку технологии крупноблочного распараллеливания SAT-задач в рамках следующих грантов РФФИ: № 04-07-90358 (2006 г.), № 07-01-00400-а (2007-2008 гг.), а также грантов поддержки ведущих научных школ: НШ-9508.2006.1 (2006 г.), НШ-1676.2008.1 (2008 г.);
в создание ШШ Distributed-SAT (D-SAT), предназначенного для параллельного решения SAT-задач: свидетельство № 2008610423 об официальной регистрации программы для ЭВМ, выданное Федеральной службой по интеллектуальной собственности, патентам и товарным знакам (2008 г.);
в учебный процесс (разработка курсовых и дипломных работ) Института математики, экономики и информатики Иркутского государственного университета (ИМЭИ ИГУ).
Копии документов о внедрении приведены в приложении 2.
Апробация работы
Результаты диссертации докладывались и обсуждались на 1-ой и 2-ой Международных научных конференциях «Параллельные вычислительные технологии (ПАВТ)» (Челябинск, 2007; Санкт-Петербург, 2008), на 4-ой Международной конференции «Параллельные вычисления и задачи управления (РАСО'2008)» (Москва, 2008), на XV Международной конференции «Вычислительная механика и современные прикладные
программные системы (ВМСППС'2007)» (Алушта, 2007), на XIV
Байкальской международной школе-семинаре «Методы оптимизации и их
приложения» (Северобайкальск, 2008 г.) на VI и VII Сибирских научных
школах-семинарах с международным участием «Компьютерная безопасность
и криптография» (Горно-Алтайск, 2007; Красноярск, 2008), на II
Всероссийской конференции с международным участием
«Инфокоммуникационные и вычислительные технологии и системы (ИКВТС'2006)» (Улан-Удэ, 2006), на 6-ой школе-семинаре «Распределенные и кластерные вычисления» (Красноярск, 2006), на научных конференциях «Ляпуновские чтения» (Иркутск, 2006; 2007), на VI и IX школах-семинарах молодых ученых «ММИТ» (Иркутск, 2005; 2007); на научных семинарах Института динамики систем и теории управления СО РАН, а также на научном семинаре кафедры защиты информации и криптографии Томского государственного университета (2008 г.).
Структура работы и личный вклад автора
Диссертация состоит из введения, трех глав, заключения и списка литературы, насчитывающего 105 наименований, изложена на 116 страницах, содержит 14 иллюстраций и 7 таблиц. Первая глава является обзорной, в ней отражены в основном известные результаты. Часть результатов второй главы (введение прогнозных функций, оценка сложности процедур прогнозирования времени параллельного решения SAT-задач) получены в неделимом соавторстве с научным руководителем. Все остальные результаты, представленные в диссертации, получены автором лично.
Публикации
Основные результаты диссертации опубликованы в восемнадцати работах, из них две публикации в изданиях, входящих в список ВАК.
Постановка SAT-задач. Сведение задач обращения дискретных функций к SAT-задачам
Булевы функции {функции алгебры логики) являются одним из основных объектов дискретной математики и математической логики (см. [1], [2]). Переменные, принимающие значения в множестве \ложъ,истина), называются логическими или булевылш. Булевой функцией от п переменных называется функция /: {ложь,истина}" - {ложъ,истина\п & N. Далее для краткости значение «ложь» обозначаем нулем, а значение «истина» единицей.
Пусть L(xu...,xn) - формула, представляющая произвольную булеву функцию от булевых переменных Х,,...,Х„. Выражения вида Дх1,...,л/1) = А/?є{0,і}, (1) называются логическими уравнениями. Решить логическое уравнение вида (1) означает найти такой набор {аъ...,ап),а( є {o,l},z є {і,...,и}, что L{xx,...,xn) на наборе (ah...,an), то есть при х1=а1,х2=а2,...,хп=ап, принимает значение р (данный факт обозначается как L(xb...,xn)\(ai а„)-Р)- Любой такой набор значений булевых переменных хх,...,хп для соответствующего логического уравнения вида (1) называется решением данного уравнения. Если такого набора не существует, то говорят, что уравнение вида (1) не имеет решений. Выражения вида \L{(xx,...,xn) = Р! (2) где р, є {ОД},...,р„, є {ОД}, называются системами логических уравнений. Решением системы вида (2) называется такой набор значений истинности переменных хх,...,хп, который является решением каждого уравнения данной системы. Если такого набора не существует, то система логических уравнений называется несовместной. Под логическим поиском далее понимаются задачи поиска решений систем логических уравнений.
Через {од}" обозначается множество всех двоичных последовательностей длины п. Дискретной функцией называется произвольная функция вида /и:{од}и- {од} ,ие , где {o,l} =JneN{o,i}". Через /о;л/"„ с {од}" обозначается
область определения функции /„, а через range fn е {од} ее область значений. Дискретную функцию /„ назовем всюду определенной если dom f„ = {од}".
В качестве формальной вычислительной модели в диссертации рассматривается детерминированная машина Тьюринга с входным алфавитом s = {o,l}. Пусть м(/) - программа для детерминированной машины Тьюринга (далее МТ-программа), которая вычисляет любую дискретную функцию из некоторого натурального семейства / = {/„}„eN всюду определенных дискретных функций. Тогда все дискретные функции из семейства / алгоритмически вычислимы (согласно тезису Черча), и для МТ-программы м(/) стандартным образом (см. [3], [4]) можно определить вычислительную сложность, как функцию от п (длины входа).
Класс з (см. [5]) образован всеми такими алгоритмически вычислимыми семействами всюду определенных дискретных функций, которые могут быть вычислены МТ-программами с полиномиальной от п вычислительной сложностью.
задачи (см. раздел 1.3).
В работе [6] С.А. Куком была предложена фундаментальная идея представления алгоритмов в виде логических уравнений. Следующая теорема (см. [5]) переносит эту идею на задачи обращения дискретных функций из класса з.
Теорема 1.1 (см. [5]).
Проблема обращения функции /„ произвольного семейства /єЗ в общем случае за полиномиальное от п время преобразуется в проблему поиска решений некоторой системы логических уравнений. Функция объема получаемого при этом семейства систем логических уравнений растет как некоторый полином от п.
Общая идея теоремы 1.1 состоит в том, что процедуру вычисления каждой функции /„,«eN, семейства /еЗ можно рассматривать как применение к произвольным входам из {ОД}" МТ-программы M(f), процесс вычисления которой можно представить в виде некоторой системы логических уравнений.
На основе теоремы 1.1 и ряда последующих результатов был развит так называемый пропозициональный подход, в контексте которого задачи обращения дискретных функций из класса 3 эффективно сводятся к задачам поиска решений систем логических уравнений (см., например, [7]).
Существуют различные подходы к решению систем логических уравнений. Перечислим некоторые из них: - сведение систем логических уравнений к системам полиномиальных уравнений над полем GF(2). Для решения таких систем можно использовать разнообразные модификации алгоритма Бухбергера (см. [8], [9]) или методы, основанные на последующем сведении к системам линейных уравнений (к таким методам относится, например, метод линеаризационного множества, предложенный и развитый в работах [10], [11], [12], [13]); - подход, использующий представления булевых уравнений в форме двоичных диаграмм решений (Binary Decision Diagrams, см. [14], [15]); - SAT-подход, описание которого приводится далее. Пусть х = {хх,...,х„) — множество булевых переменных. Термы X, И X, , /є{і,...,и}, называются литералами над X (через х обозначается логическое отрицание х). Литералы х и х называются контрарными.
Методы и алгоритмы решения SAT-задач
Для решения SAT-задач используются специализированные программные комплексы, называемые SAT-решателями. SAT-решатели могут использовать в качестве основы различные алгоритмы (см. [27]). Рассмотрим следующие классы таких алгоритмов: 1. Алгоритмы, основанные на методе резолюций (см. [20], [21], [28]). 2. Алгоритмы, использующие «оптимизационную семантику» (MAXSAT-алгоритмы, алгоритмы, основанные на локальном и глобальном поиске, и др., см. [27], [29]). 3. Алгоритмы, основанные на DPLL (см. [19], [30], [31]). Во всех приведенных выше алгоритмах рассматривается произвольная КНФ C = Dr..,Dm (9) в которой Dj,j e{l,...,m} - это дизъюнкты над множеством булевых переменных X = {хх,...,хп}. Требуется решить SAT-задачу для КНФ С . Алгоритмы, основанные на методе резолюций
Метод резолюций впервые был описан Дж. А. Робинсоном в работе [20]. Ниже приводится краткое описание основы этого метода. Пусть дана КНФ вида (9). Дизъюнкты Д. и Dki, кх,к2 e{i,...,m] называются контрарными по паре {х,х},х =Х, если Dki и Dk2 содержат х я х (т.е. Dki содержит х, a Dki содержит х или наоборот - Dk{ содержит х, a Dh содержит л). Пусть D — произвольный дизъюнкт и а - литерал, входящий в D. Через D \ {а} обозначается дизъюнкт, полученный из D вычеркиванием а. Пусть Dk и Dk , kx,k2&\[,...,m} контрарны по паре {х,х\хєХ. Дизъюнкт D =(z)fci \{x}vDk2 \{х}) называется резольвентой дизъюнктов DK и Dki. Пусть D — резольвента некоторой пары дизъюнктов из с. Тогда КНФ С=С-П выполнима на тех и только тех наборах значений истинности переменных из X, на которых выполнима с.
Описанная процедура представляет собой одну итерацию метода резолюций. В работе [20] было показано, что С невыполнима тогда и только тогда, когда существует такая конечная последовательность итераций метода резолюций, итогом которой является пустой дизъюнкт. Пустой дизъюнкт (не содержащий литералов) является резольвентой единичных контрарных ДИЗЪЮНКТОВ ВИДа а И а . Алгоритмы, использующие оптимизационную семантику
В основе такого рода алгоритмов лежит рассмотрение SAT-задачи как задачи дискретной оптимизации (см. [27]). Рассматривается произвольная КНФ вида (9). Вводится функционал вида Ыс(а), а є {0,1}" , значение которого равно числу дизъюнктов в (9), истинных на векторе а , Очевидно, что -тах„ №с (а) - т, тогда и только тогда, когда КНФ С ссє{0Д} выполнима (в этом случае любой вектор, доставляющий максимум функционалу Мс(а) - это вектор, выполняющий С ). КНФ С невыполнима тогда и только тогда, когда _тах №с (а) т . Таким образом, SAT-задача ае{0,1}" для произвольной КНФ С вида (9) сводится к задаче максимизации функционала Иг(0 на множестве {0,l}". Алгоритмы, основанные на DPLL
Подавляющее большинство современных SAT-решателей, показывающих высокие результаты на специализированных конкурсах (см. [32]), базируются на алгоритме DPLL (см. [30]). Далее в диссертации рассматриваются только такие SAT-решатели.
В настоящее время в развитии эффективных алгоритмов на основе DPLL принято выделять следующие три этапа. - 1962 г. Алгоритм DPLL (бэктрекинг, ВСР-стратегия). - 1999 г. Алгоритм GRASP (бэкджампинг, CL-процедура). - 2001-2008 гг. Дальнейшие усовершенствования алгоритмов на основе DPLL (эвристики выбора значений угадываемых переменных, процедуры чистки базы конфликтных дизъюнктов, рестарты, быстрые структуры данных и т.д.).
Далее приведено описание алгоритма DPLL, а также некоторых технологий, позволяющих существенно ускорять DPLL-вывод (эти технологии подробно рассмотрены в обзоре [17]).
Алгоритм DPLL. В 1962 г. М. Девис, Дж. Лонджман и Д. Лавленд в работе [30] предложили алгоритм DPLL (в некоторых источниках используется сокращение DLL). Алгоритм DPLL основывался на процедуре, предложенной в 1960 г. М. Дэвисом и X. Патнемом в работе [19]. Ниже приведено описание алгоритма DPLL.
Рассмотрим произвольную КНФ вида (9). Угадывание состоит в выборе некоторой переменной Xf &{хи...,хп}, присвоения ей произвольного значения и подстановки данного значения в КНФ С. Переменную х, назовем назначенной переменной, все остальные переменные называются неназначенными. Угадывание осуществляется из множества неназначенных переменных. КНФ при этом рассматривается как система (база) ограничений—дизъюнктов. Ограничения, которые представляют собой некоторые дизъюнкты КНФ С, могут не удовлетворять значению истинности назначенных переменных. В таком случае дизъюнкты принимают значение «0», и данный факт обозначается как конфликт. Так, дизъюнкт (xl v х4) принимает значение «0» в результате присвоений =0,х4=0, а дизъюнкт (x2 vx3 vx4) - в результате присвоений X = 1, X3 = U, X4 — 1.
Последовательность угадываний организуется в виде нумерованного списка уровней решения {decision level). Переменная, значение которой угадывается на данном уровне решения, называется переменной решения этого уровня. В случае конфликта происходит так называемый бэктрекинг {backtracking), т.е. откат на один шаг назад (значение последней назначенной переменной меняется на противоположное). Если же оба варианта присвоения последней назначенной переменной, кроме первой, скажем, xi+l,ie{l,...,n-l}, приводят к конфликту, то при бэктрекинге происходит откат еще на один уровень назад, то есть возвращение к моменту выбора значения для переменной xt,i є (1,..., и-1), с последующим изменением значения х, на противоположное.
Методы параллельного решения SAT-задач
Далее приводятся некоторые определения из теории параллельных вычислений (см. [59], [60], [61]).
Распределенная вычислительная среда (РВС) — совокупность вычислительных узлов, объединенных коммуникационной сетью.
Вычислительный узел РВС - программно-аппаратный ресурс, включающий модуль оперативной памяти, один или несколько процессоров, жесткий диск и системное программное обеспечение (ПО).
Вычислительный кластер (далее кластер) — это РВС, в которой все вычислительные узлы объединены единой коммуникационной сетью.
Вычислительная единица РВС — программно-аппаратный ресурс, требуемый для решения некоторой вычислительной задачи. В качестве вычислительной единицы в диссертации рассматривается одно ядро процессора, часть общей оперативной памяти и памяти жесткого диска, а также системное ПО. Выбор именно таких характеристик вычислительной единицы обусловлен тем фактом, что в современных программных SAT-решателях основная нагрузка приходится на процессор.
Главная (управляющая) единица РВС — одна из вычислительных единиц РВС, обладающая функциями управления заданиями пользователей и ресурсами РВС.
Обычно выделяют два вида параллелизма — мелкозернистый (см. [62]) и крупноблочный (см. [63]).
Мелкозернистый параллелизм характеризуется большим количеством параллельно выполняемых простых, часто одинаковых, вычислений, обмен результатами при этом происходит на каждом шаге. Мелкозернистый параллелизм зачастую характеризуется невысокой масштабируемостью. Тем не менее, мелкозернистый подход с успехом используется при вычислительном моделировании различных динамических процессов (см., например, [64]).
Крупноблочный параллелизм характеризуется небольшим числом сложных последовательных вычислений с редкими обменами промежуточными результатами. При этом параллельными фрагментами являются отдельные задачи, информационно несвязанные либо слабо связанные между собой. Такой уровень параллелизма характерен, например, для grid-систем (см. [65]). При этом РВС свободна от ряда ограничений, присущих мелкозернистому параллелизму (таких как однородность вычислительных узлов и единая коммуникационная сеть). Кроме этого, крупноблочный подход, как правило, характеризуется высокой масштабируемостью. Одной из первых работ по применению крупноблочного параллелизма в решении практически важных задач является статья [66].
Следует отметить, что деление параллелизма на мелкозернистый и крупноблочный весьма условно. В некоторых задачах обмен данными происходит далеко не на каждом «элементарном шаге». Однако общее число обменов весьма существенно, что может оказывать решающее влияние на масштабируемость задачи (см., например, [67]).
Реализация концепции мелкозернистого параллелизма в отношении SAT-задач приводит к необходимости распараллеливания на уровне базового алгоритма SAT-решателя (SAT-решатели с параллельной вычислительной архитектурой). Данный подход представлен, например, в работе [68], в которой описана параллельная реализация алгоритма DPLL. Фактически первые параллельные SAT-решатели, основанные на мелкозернистом подходе, появились совсем недавно (конкурс SAT-Race 2008, см. [69]). Отметим, что современные SAT-решатели являются довольно сложными в структурном смысле программами (см. раздел 1.2), в связи с чем реализация мелкозернистого подхода трудна в техническом отношении. Также при мелкозернистом подходе значительная часть ресурсов РВС расходуется на обмен данными между вычислительными узлами. Сказанное подтверждается тем фактом, что все представленные на SAT-Race 2008 решатели задействовали в своей работе ресурсы одного четырехядерного процессора.
Крупноблочный параллелизм предпочтителен в решении SAT-задач с некоторым известным множеством булевых переменных, от которых «информативно зависят» все остальные переменные КНФ. Для таких SAT-задач размерность пространства полного перебора существенно меньше числа булевых переменных, фигурирующих в КНФ. Речь идет, прежде всего, о SAT-задачах, к которым сводятся задачи обращения дискретных функций из класса з (см. раздел 1.3). Далее в диссертации развивается именно такой вид параллелизма. Результатом является описанная в разделах 2.2, 2.3 и 2.4 крупноблочная параллельная технология решения SAT-задач в РВС. Технология понимается как совокупность математических и инженерных методов обработки информации в соответствующей предметной области.
В разделе 2.2 предлагается методика крупноблочного распараллеливания SAT-задач. В разделе 2.3 предлагается процедура статистического прогнозирования трудоемкости параллельного решения SAT-задач при их крупноблочном распараллеливании. В разделе 2.4 анализируются различные стратегии построения декомпозиционных представлений SAT-задач.
Библиотека программ пакета D-SAT
Библиотека программ пакета D-SAT включает следующие модули, реализованные на языке C++: - модуль расщепления (далее ml); - модуль SAT-решателя (далее ml); - модуль прогнозирования (далее тЗ); - модуль сравнения (далее т4); - аналитический модуль (далее т5); - транспортный модуль (далее тб).
Все модули пакета являются платформонезависимыми (в смысле переносимости на уровне исходного кода, см. [86], [87]) и могут выполняться под управлением Unix-подобных операционных систем (ОС), а также под управлением ОС семейства Windows.
Модуль расщепления используется для декомпозиции исходной SAT-задачи на семейство подзадач. В данном модуле реализован ряд схем формирования (в частности, схемы формирования, предложенные в разделе 2.4). При этом каждой схеме формирования яу, соответствует определенный натуральный номер j є {і,..., р]. Основные входные данные модуля расщепления следующие: - файл с исходной КНФ в формате DIMACS [88]; - номер je{l,...,p} схемы формирования; - диапазон значений dy (левая и правая границы); - фиксированное значение j, определяющее число КНФ в произвольной случайной выборке.
Обозначим через dfn и dax натуральные числа, определяющие соответственно нижнюю и верхнюю границы интервала, в котором изменяются значения dr Для каждого значения djefay,... 3 } строится
отдельное семейство КНФ. В случае q 2dj из декомпозиционного семейства случайным образом выбираются q КНФ. Если q = 0 или q 2dj, то выборкой является все рассматриваемое семейство. Результатом декомпозиции является набор файлов с КНФ (см. раздел 2.2), представленными в формате DIMACS. Этот набор в комплексе DISCOMP описывается в виде параллельного списка (см. [70], [71], [84]).
Модуль SAT-решателя по входному файлу, в котором исходная КНФ представлена в формате DIMACS, осуществляет поиск выполняющего данную КНФ набора, либо выдает значение NULL в случае отсутствия такового (т.е. решает SAT-задачу для исходной КНФ). В выходной файл каждой копии модуля SAT-решателя записывается информация о результатах его работы (подробности препроцессинга, количество и характеристики проведенных рестартов, время вычисления, решение SAT-задачи).
Модуль прогнозирования Основные входные данные модуля прогнозирования следующие: - файлы с результатами работы модуля SAT-решателя; -значение q\ - число г вычислительных единиц РВС, относительно которого строится прогноз. Модуль прогнозирования производит статистический анализ входных данных, на основе которых строится прогноз оптимального (с точки зрения вычислительных затрат) значения dj (обозначим такое прогнозное значение через dj). При этом дополнительно учитываются все транспортные расходы. Модуль сравнения получает на вход прогнозные значения d x,...d и выдает значение d є {dx,...d p} с наилучшим прогнозом, а также соответствующий значению d" номер схемы формирования / є {],..., р}.
Аналитический модуль вычисляет среднее, минимальное и максимальное время решения SAT-задач для списка КНФ, сравнивает прогнозное время решения с реальным временем. Если исходная КНФ оказалась выполнимой, модуль проверяет найденный выполняющий набор на корректность (путем его подстановки в исходную КНФ). Решение SAT-задачи и результаты анализа записываются в итоговый выходной файл.
Транспортный модуль осуществляет необходимый для пакета D-SAT обмен данными между вычислительными единицами РВС. Основной задачей данного модуля является рассылка КНФ из параллельного списка. Функционирование транспортного модуля подробно рассматривается в разделе 3.1.3. Пакет D-SAT может функционировать в следующих режимах: - режим прогнозирования; - режим решения SAT-задачи; - режим прогнозирования с последующим решением SAT-задачи. Режим прогнозирования
В данном режиме для каждой схемы формирования с номером je\h„...,p} выполняются следующие шаги (см. рис. 3.1).
1. На вход модулю расщепления подается файл с исходной КНФ в формате DIMACS, номер je{\,...,p} способа формирования, диапазон значений dj, а также число г вычислительных единиц РВС, относительно которого строится прогноз. Модуль расщепления для каждого значения dj є jtf"1,..., 4} строит соответствующую выборку КНФ с учетом значений q и je{l,...,p}. Полученные файлы КНФ в формате DIMACS объединяются в параллельный список и передаются на модуль SAT-решателя.
2. Для каждой КНФ полученного параллельного списка с помощью модуля SAT-решателя решается соответствующая SAT-задача -доказывается невыполнимость либо находится выполняющий набор.
3. После того как решены SAT-задачи для всех КНФ из параллельного списка, при помощи модуля прогнозирования производится статистический анализ полученных результатов (с учетом значения г), и на его основе вычисляется d є jd/j"111,..., 3 } - прогноз оптимального значения dj для способа формирования с номером Л.
По вычисленным значениям d x,...,d p модуль сравнения определяет значения d є \l x,...,d p} и / є {і,...,р] с наилучшим прогнозом (см. рис. 3.2).
В режиме прогнозирования существует возможность того, что будет найден набор, выполняющий исходную КНФ. В этом случае решение задачи считается найденным, и вычислительный процесс завершается (прерывается решение для всех SAT-задач из параллельного списка).
