Введение
1 Основные понятия 19
1.1 Системы доказательств 19
1.2 DPLL-алгоритмы 1.2.1 Связь с системами доказательств 23
1.2.2 "Пьяные" и "близорукие" алгоритмы 24
1.3 Функция Голдрейха 25
1.3.1 Формулы, построенные по функции Голдрейха 26
1.4 Экспандеры 27
1.5 Распределения на входах 28
2 Нижние оценки на сложность обращения функции Гол дрейха близорукими DPLL-алгоритмами 30
2.1 Почти биективная функция Голдрейха 31
2.1.1 Линейная функция 31
2.1.2 Немного нелинейная функция Голдрейха
2.2 Нижняя оценка времени работы на невыполнимых формулах 33
2.3 Нижняя оценка времени работы на выполнимых формулах 35
2.3.1 -замыкание
2.3.2 "Умный" близорукий алгоритм 38
3 Нижние оценки на близорукие DPLL-алгоритмы с эври стикой отсечения 44
3.1 DPLL-алгоритмы с эвристикой отсечения 45
3.2 Система близоруких копий 47
3.3 Граничный экспандер и линейное замыкание 50
3.4 Очищенное дерева поиска
3.4.1 Универсальное распределение 56
3.4.2 Нижняя оценка на выполнимых формулах 57
3.5 Конструкция экспандера 57
4 Нижние оценки для расщепления по линейным комбина циям 60
4.1 Деревья расщеплений по линейным формам 61
4.2 Верхние оценки 63
4.3 Нижняя оценка для 2-кратных цейтинских формул
4.3.1 Коммуникационный протокол из дерева линейных расщеплений 65
4.3.2 Нижняя оценка на коммуникационную сложность
4.4 Нижняя оценка для принципа Дирихле 69
4.5 Системы доказательств Res-Lin и Sem-Lin
4.5.1 Древовидная Res-Lin и деревья линейных расщеплений 76
4.5.2 Импликативная полнота Res-Lin 78
4.5.3 Моделирование Res-Lin в R{lin) 80
Литература
