Сложность решения задачи выполнимости булевых формул алгоритмами, основанными на расщеплении

• Автор: Соколов, Дмитрий Олегович
• Шифр специальности: 01.01.06, 01.01.09
• Научная степень: Кандидатская
• Год защиты: 2014
• Место защиты: Санкт-Петербург
• Количество страниц: 88 с.

Оглавление
Введение

Системы доказательств

БРЬЬ-алгоритмы

Экспандеры

Односторонние функции

Структура диссертации

1 Основные понятия

1.1 Системы доказательств

1.2 БРЬЬ-алгоритмы

1.2.1 Связь с системами доказательств

1.2.2 “Пьяные” и “близорукие” алгоритмы
1.3 Функция Голдрейха
1.3.1 Формулы, построенные по функции Голдрейха
1.4 Экспандеры
1.5 Распределения на входах
2 Нижние оценки на сложность обращения функции Голдрейха близорукими БРЬЬ-алгоритмами
2.1 Почти биективная функция Голдрейха
2.1.1 Линейная функция
2.1.2 Немного нелинейная функция Голдрейха
2.2 Нижняя оценка времени работы на невыполнимых формулах
2.3 Нижняя оценка времени работы на выполнимых формулах
2.3.1 /с-замыкание

2.3.2 “Умный” близорукий алгоритм
3 Нижние оценки на близорукие DPLL-алгоритмы с эвристикой отсечения
3.1 DPLL-алгоритмы с эвристикой отсечения
3.2 Система близоруких копий
3.3 Граничный экспандер и линейное замыкание
3.4 Очищенное дерева поиска
3.4.1 Универсальное распределение
3.4.2 Нижняя оценка на выполнимых формулах
3.5 Конструкция экспандера
4 Нижние оценки для расщепления по линейным комбинациям
4.1 Деревья расщеплений по линейным формам
4.2 Верхние оценки
4.3 Нижняя оценка для 2-кратных цейтинских формул
4.3.1 Коммуникационный протокол из дерева линейных расщеплений
4.3.2 Нижняя оценка на коммуникационную сложность .
4.4 Нижняя оценка для принципа Дирихле
4.5 Системы доказательств Res-Lin и Sem-Lin
4.5.1 Древовидная Res-Lin и деревья линейных расщеплений
4.5.2 Импликативная полнота Res-Lin
4.5.3 Моделирование Res-Lin в R(lin)
Литература

Введение
Задача выполнимости булевых (пропозициональных) формул (SAT) — это задача нахождения по булевой формуле такой подстановки значений переменным, что при применении данной подстановки формула обращается в тождественную истину. Если такая подстановка существует, то формула называется выполнимой; если же нет, то функция, задаваемая данной формулой, является тождественной ложью, и формула является невыполнимой.
SAT - одна из первых задач, для которых была доказана NP-полнота (теорема Кука-Левина [1, 2]). Это означает, что любая задача из класса NP, который включает в себя широкий круг естественных задач, возникающих на практике, сводится к задаче выполнимости булевых формул. Таким образом, существование эффективного алгоритма для SAT эквивалентно одной из центральных задач теории сложности о равенстве между классами Р и NP, и таких алгоритмов в настоящее время не известно.
Несмотря на это, формулы, возникающие на практике, успешно решаются при помощи эвристических SAT-солверов (программ для решения задачи выполнимости). В данной работе мы рассмотрим общую схему работы большинства современных SAT-солверов — алгоритмы расщепления, идея которых восходит к работам [3, 4]. Также мы рассмотрим криптографический аспект, а именно, возможности алгоритмов расщепления по взлому функции Голдрейха [5] кандидата на роль односторонней функции. Также мы рассмотрим системы доказательств, связанные с алгоритмами расщепления.
Классическими примерами формул, которые сложны для алгорит-

V € А, которая не входит в дизъюнкт С. Рассмотрим множество Л{-у}, из него семантически не следует дизъюнкт С, значит существует такое значение переменных, при которых все формулы из А {г>} истинны, а С ложно. Но заменой значения переменной х3 легко сделать, чтобы все формулы из А были бы истинны, а С ложно, противоречие с тем, что С семантически следует' из А. □
Следствие 2.2 ([24]). Размер дерева расщеплений для формулы Ф|р не меньше 2*£тЙ2Нр1~'г.
Доказательство. Следует из теоремы 2.2, теоремы 1.4 и предложения 1.1. □
2.3 Нижняя оценка времени работы на выполнимых формулах
2.3.1 /с-замыкание
Пусть граф Д - граничный (г, ф с)-экспандер. Пусть 0 < к < с — 2.
Предикат Р(жь ..., хД = XI 4-----+ ха-к + Я{х<1-к+ъ • ■ •, хй) функция
Голдрейха / задана графом С и предикатом Р.
Определение 2.1 ([22]). Пусть «/ С X, множество вершин I С Р будем называть Аьзамыканием множества J, если существует такая конечная последовательность множеств /], /2,..., 1т (обозначим С = икг Со = 0), что выполняются следующие свойства:
• ф С У и 0 < |ф| < | для всех 1 < I < т;
• 1{ П I] = 0 для всех 1 <1..) < т;
• |4(ф) (Г(С^_х) и «7)| < (1 + &)|ф| для всех 1 < I < т;
• для всех V С У Сто, если 0 < |7;| < то |£(/') (Г(С7„) и «7)| > (1 + к)1']