Введение
1 Основные понятия 20
1.1 Основные обозначения 20
1.2 Классы сложности 21
1.3 Системы доказательств
1.3.1 Язык UNSAT 23
1.3.2 Резолюционная система доказательств 24
1.3.3 Система доказательств секущих плоскостей 25
1.3.4 Система доказательств полиномиального исчисления 26
1.3.5 Резолюционная система доказательств с резолюцией по линейным формам Res-Lin 27
1.4 Алгоритмы для SAT и деревья расщеплений 27
1.4.1 DPLL алгоритм 27
1.4.2 Алгоритм линейных расщеплений 29
1.5 Задача выполнения ограничений 30
1.6 Графы 33
2 Верхние оценки для резолюционных систем доказательств 34
2.1 Формулы для принципов Дирихле и совершенного паросо четания 35
2.1.1 Принцип Дирихле 35
2.1.2 Принцип совершенного паросочетания
2.2 Верхняя оценка на принцип совершенного паросочетания в общей резолюции 37
2.3 Верхние оценки на древовидные доказательства в системе Res-Lin
2.3.1 Принцип Дирихле 41
2.3.2 Принцип совершенного паросочетания 46
3 Резолюционные системы доказательств над произвольным алфавитом 50
3.1 Нижняя оценка на минимальную ширину доказательств в системе NG-Res 51
3.2 Обобщенные цейтинские формулы 53
3.3 Нижняя оценка на обобщенные цейтинские формулы
3.3.1 Сокращенное дерево расщеплений 56
3.3.2 Нижняя оценка 58
3.4 Верхняя оценка на древовидные резолюционные доказа тельства 60
4 Доказательствасправилом сдвига 64
4.1 Подвижные формулы и системы доказательств с правилом сдвига 65
4.2 Нижние оценки на размер доказательств с правилом сдвига
4.2.1 Кодировка 68
4.2.2 Нижние оценки для систем, устойчивых к замене переменных 70
4.2.3 Устойчивость к замене переменных 75
4.3 Разделение систем доказательств с правилом сдвига и без
него 79
4.3.1 Формула–счетчик 79
4.3.2 Верхняя и нижняя оценки 81
Заключение 87
Литература
