Введение
1 Определения 10
1.1 Задачи булевой логики 10
1.1.1 Формулы в КНФ 10
1.1.2 Задачи выполнимости и максимальной выполнимости 12
1.2 Алгоритм расщепления 14
1.3 Анализ алгоритмов расщепления 17
1.4 Класс формул 19
2 Методы доказательства верхних оценок, использующиеся в работе 23
2.1 Пример простого алгоритма расщепления 24
2.2 Общее правило упрощения 26
2.3 Автоматический анализ сложности алгоритмов расщепления 28
2.4 Комбинированные меры сложности 29
2.5 Запоминание дизъюнктов 33
3 Автоматическое порождение правил упрощения 35
3.1 Известные правила упрощения для SAT и MAX-SAT 35
3.2 Общее правило упрощения 37
3.3 Алгоритм для (n, 3)-MAX-SAT 44
4 Автоматический анализ времени работы 50
4.1 Описание программы 50
4.1.1 Входные и выходные данные 51
4.1.2 Алгоритм построения доказательства 54
4.1.3 Детали реализации 57
4.1.4 Правила упрощения 60
4.1.5 Правило расщепления 60
4.1.6 Мера сложности 61
4.1.7 Инвариант 61
4.2 Автоматически доказанные верхние оценки 62
4.3 Подобные работы 64
5 Комбинированные меры сломсности и запоминание дизъюнктов 67
5.1 Решение MAX-SAT на формулах константной плотности быстрее, чем за 2N 67
5.2 Алгоритм для MAX-2-SAT 71
5.2.1 Правила упрощения 72
5.2.2 Правила расщепления 76
5.2.3 Алгоритм для MAX-2-SAT 78
5.2.4 (n, 3)-М AX-2-SAT 83
