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

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

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

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

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

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

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

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

Метод резолюций, схема реализации: По мере появления, резольвенты длины не более 3 добавляются к исходной КНФ и могут быть использованы для вычисления других резольвент. Дублирующие скобки и тавтологии удаляются. Скобки, содержащие 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 α2α2 α3α3 α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^610^60,70,20,10210:45:13

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

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

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

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

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

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

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

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

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