« АЛГОРИТМ МИНИМИЗАЦИИ ФУНКЦИОНАЛА, АССОЦИИРОВАННОГО С ЗАДАЧЕЙ SAT И ЕГО ПРАКТИЧЕСКИЕ ПРИМЕНЕНИЯ » Омский государственный университет им. Ф.М.Достоевского В.И. Дулькейт, Е.В. Салаев, Р.Т. Файзуллин, И.Г. Хныкин

ЦЕЛЬ РАБОТЫ Сведение задачи SAT к проблеме минимизации ассоциированного функционала специального вида. Построение распараллеливаемых методов минимизации функционала. Практическое применение построенных алгоритмов в задачах асимметричного криптоанализа.

ПОСТАНОВКА ЗАДАЧИ Дано: пропозициональная формула в конъюнктивной нормальной форме на множестве переменных. Задача ВЫПОЛНИМОСТЬ (SAT): найти решающий набор такой, что принимает значениеИСТИНА.

Переход от задачи ВЫПОЛНИМОСТЬ к задаче поиска глобального минимума функционала

Дифференцируя функционал F (x), отвечающий эквивалентной 3-ДНФ, по всем переменным, получаем систему уравнений:

Модифицированный метод последовательных приближений Метод последовательных приближений

МЕТОДЫ ГИБРИДИЗАЦИИ, ПРИМЕНЯЕМЫЕ С ЦЕЛЬЮ УЛУЧШЕНИЯ СХОДИМОСТИ Метод резолюций Метод резолюций Смещение по антиградиенту функционала Смещение по антиградиенту функционала Методика смены траектории Методика смены траектории Методика экстраполяции Методика экстраполяции Увеличение разрядности вычислений Увеличение разрядности вычислений

Метод резолюций Метод резолюции позволяет получить эквивалентную КНФ, в которой количество скобок и переменных меньше, чем в исходной. Если две скобки КНФ обладают таким свойством, что переменная х входит в одну из них с отрицанием, а в другую без, то резольвентой будем называть дизъюнкцию скобок без переменной х и ее отрицания.

Метод резолюций, схема реализации: По мере появления, резольвенты длины не более 3 добавляются к исходной КНФ и могут быть использованы для вычисления других резольвент. По мере появления, резольвенты длины не более 3 добавляются к исходной КНФ и могут быть использованы для вычисления других резольвент. Дублирующие скобки и тавтологии удаляются. Скобки, содержащие 1 литерал, используются для разрешения переменной. Дублирующие скобки и тавтологии удаляются. Скобки, содержащие 1 литерал, используются для разрешения переменной. Процедура продолжается до тех пор, пока не будут вычислены все резольвенты. Процедура продолжается до тех пор, пока не будут вычислены все резольвенты.

Метод резолюций, результаты Для КНФ, эквивалентных задаче факторизации удается уменьшить количество скобок в среднем на 30 % и разрешить около 0.5% переменных. число бит в сомино- жителе число переменных в КНФ число скобок в КНФ число скобок после вычисления резолюций время вычисления резолюций : 00 : : 00 : : 00 : : 01 : : 11 : : 31 : 27

Смещение по антиградиенту функционала Рассмотрим итерационную формулу: Вектор x(t) является решением, если только p=0. Следовательно, к приближению необходимо добавить поправку:

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

Методика экстраполяций Анализируется поведение значений компонент последовательности векторов. Анализируется поведение значений компонент последовательности векторов. На основе этого экстраполируется конечное значение. На основе этого экстраполируется конечное значение. ЭВРИСТИКА Если компонента вектора больше 0.5 и монотонно возрастает, то можно сделать вывод, что в векторе решении она равна 1, и наоборот. Данная эвристика приводит к успеху в 70% случаев.

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

РАСПАРАЛЛЕЛИВАНИЕ, способ 1 Необходимо наличие нескольких эквивалентных КНФ. Вычисления проводятся по схеме: Z X Z 0 =X k Y 0 =Z k X 0 =Y k Y

РАСПАРАЛЛЕЛИВАНИЕ, способ 2 ДНФ, эквивалентная исходной КНФ делится на K-подформул. Для каждой под формулы ищется решение. Полученные вектора решений образуют K-угольник. На стороне K-угольника выбираются n-мерные точки x так, чтобы минимизировать F(x). Вектор х подставляется в качестве начального приближения для итерационной процедуры, которая запускается для функционала, ассоциированного со всей формулой.

Результаты, КНФ, сгенерированные случайно число скобок число переменных α1α1α1α1 α2α2α2α2 α3α3α3α3 α4α4α4α4 кол-во итераций время работы ,60,250,10,530:0: ,70,20,1040:0: ,60,250,10,570:0: ,70,20,1050:0: ,60,250,10,560:0: ,70,20,1040:0: ,60,250,10,570:2: ,70,20,1080:2:30 210^6 10^6 0,70,20,10210:45:13

Результаты, параллельный алгоритм Наименование теста Кол-во литералов (N) Кол-во скобок (M) % решенных тестов Максимальное число итераций (часть формулы) Максимальное число итераций (вся формула) RTIBMS < sat sat sat uf20-91uf

Результаты, КНФ, эквивалентные задаче факторизация число бит в соминожителе число переменных в КНФ число скобок в КНФ Время решения сек сек мин. 2 мин мин. 7 мин мин. 36 мин часа часа часов. 6 часов мин. 36 мин часа.

Результаты, КНФ, из библиотеки SATLib Тесты Число литера- лов Числоскобок Число тестов Время решения группы All-Interval Series (AIS) 60 – – мин 36 с 4 мин 36 с Blocks World Planning 48 – – с 23 с Backbone-minimal Sub 100< с 6 с Control Backbone Size (CBS_b10 + CBS_b90) с 5 с Uniform Random мин 49 с 9 мин 49 с "Flat" Graph Coloring мин 14 с "Morphed Graph Colouring с 2 с

Общая схема решения задачи факторизации путём сведения к задаче выполнимости. 3. Подстановка бит введённого числа, упрощение формулы. 2. Генерация КНФ, эквивалентной операции умножения. 1. Ввод числа. n=pq p,q - ? 4. Сохранение в файл формата DIMACS. 5. Решение формулы с помощью внешней программы. 6. Выделение битов результата из полученного решения. p, q.

Дискретное логарифмирование. * * Операции в фигурных скобках выполняются численно. * Операции в фигурных скобках выполняются численно. Операции, представляемые в КНФ: 1. Умножение. 2. Возведение в однобитовую степень. 3. Приведение по модулю.

1., где A, B, C – логические выражения. 2., где - бит переноса. 3. (3). 4. (4). Основные операции.

Генерация КНФ для задачи факторизации. Количество бит в факторизуемом числе. Количество литералов. Количество скобок в КНФ. Время генерации ,2E3 00:00: ,2E3 00:00: ,2E600:02: E30,78E600:06: ,13E63,1E600:44: ,5E6 12,6E6 02:03:53

Генерация КНФ эквивалентной задаче дискретного логарифмирования. Количество бит. Количество литералов. Количество скобок в КНФ. Время генерации. 104,7E368E3 00:00:35 128,2E30,12E6 00:00: E30,2E6 00:01: E30,3E6 00:01: E30,44E6 00:02: E3 0,62E6 00:03:22

Зависимость числа скобок от количества бит N Скобок =O(N 2 )

Зависимость числа скобок от количества бит для задачи факторизации N Скобок =O(N 3 )

ЗАКЛЮЧЕНИЕ Построены распараллеливаемые итерационные процедуры, позволяющие решать большие системы нелинейных уравнений, ассоциированные с различными классами КНФ. Построены полиномиальные алгоритмы сведения задачи факторизации и задачи дискретного логарифмирования к КНФ. Показана применимость разработанных алгоритмов к решению задач логического криптоанализа, где ключевая информация отвечает части решающего набора КНФ.