Город: Санкт-Петербург Казань Язык: Русский English

Сложность пропозициональных доказательств
Санкт-Петербург / осень 2017, посмотреть все семестры

Запишитесь на курс, чтобы получать уведомления и иметь возможность сдавать домашние задания. Для записи требуется регистрация на сайте.
Перейти к регистрации Войти

Дана система линейных нестрогих неравенств с целыми коэффициентами. Чтобы доказать, что эта система имеет вещественное решение, можно просто его предъявить. А как доказать, что система несовместна? Это сделать можно, например, с помощью леммы Фаркаша, которая утверждает, что если система нестрогих линейных неравенств несовместна, то можно сложить эти неравенства с неотрицательными коэффициентами и получить противоречивое неравенство \(0\ge 1\). Например, система \(\left\{\begin{aligned}x+y&\ge 5 \\ -x+y&\ge -2 \\x-3y&\ge 0\\ \end{aligned}\right.\) несовместна, и если сложить первое уравнение с коэффициентом 1, второе с коэффициентом 2, а третье с коэффициентом 1, то получится \(0\ge 1\). Доказательством несовместности будет как раз этот набор неотрицательных коэффициентов.

Что, если вместо систем рассматривать логические формулы исчисления высказываний? Доказать выполнимость формулы можно точно так же – предъявив значения переменных. А можно ли коротко (полиномиально от ее длины) доказывать невыполнимость таких формул? Если такого способа доказательств нет, то классы сложности NP и coNP различаются, и, в частности, различаются классы сложности P и NP. Основная программа исследований в теории сложности доказательств заключается в доказательстве суперполиномиальных нижних оценок для как можно более мощных систем доказательств.

Пропозициональная сложность доказательств напрямую связана с алгоритмами для задачи выполнимости булевой формулы. Так, алгоритмы, расщепляющие формулу, эквивалентны древовидным резолюционным доказательствам, а современные используемые на практике алгоритмы, запоминающие дизъюнкты и обрабатывающие конфликты, соответствуют резолюционным доказательствам общего вида; полуалгебраические системы доказательств тесно связаны с алгоритмами комбинаторной оптимизации – линейным и полуопределенным программированием, а алгоритмы, основанные на базисах Гребнера, связаны с исчислением полиномов.

Примерная программа курса:

  1. Метод резолюций
    • Полнота и корректность метода резолюций
    • Древовидные системы доказательств и деревья решений. Принцип Дирихле. Нижние оценки для деревьев решений с помощью игр Прувера и Делэйера
    • Игровая интерпретация общего метода резолюций. Нижняя оценка на принцип Дирихле
    • Ширина резолюционного доказательства. Связь ширины и размера доказательств. Нижние оценки для цейтинских формул
    • Комбинаторная характеризация ширины. Память, используемая системами доказательств
    • Глубина резолюционного доказательства. Игры с фишками. Ксорификация, разделение древовидной и обычной резолюции
    • Резолюции и CDCL-солверы
  2. Исчисление полиномов
    • Нижняя оценка на степень вывода
    • Связь степени вывода и размера вывода
  3. Использование схемной сложности для доказательства нижних оценок
    • Монотонная интерполяция для метода резолюций и ее обобщение для семантических систем доказательств
    • Вещественная монотонная интерполяция для секущих плоскостей
  4. Использование коммуникационной сложности для доказательства нижних оценок
    • Нижние оценки на древовидные семантические системы доказательств
    • Компромисс между памятью и размером доказательств
  5. Системы Фреге
    • Эквивалентность систем Фреге
    • Лемма о переключении. Нижняя оценка для систем Фреге ограниченной глубины
  6. Структурные вопросы
    • Непересекающиеся NP-пары, каноническая NP-пара системы доказательств
    • Оптимальные системы доказательств и оптимальный алгоритм
    • Автоматизируемость (поиск доказательств)

Курс входит в магистерскую программу теоретическая информатика Академического университета.

Текущая версия конспекта: тут.

Дата и время Название Место Материалы
12 сентября
18:30–20:00
Лекция 1. Деревья решений, лекция ПОМИ РАН другие
12 сентября
20:20–21:50
Практика 1., семинар ПОМИ РАН файлы
19 сентября
18:30–20:00
Лекция 2. Метод резолюций, лекция ПОМИ РАН Нет
19 сентября
20:20–21:50
Практика 2., семинар ПОМИ РАН файлы
26 сентября
18:30–20:00
Лекция 3., лекция ПОМИ РАН Нет
26 сентября
20:20–21:50
Практика 3., семинар ПОМИ РАН файлы
13 сентября 2017

Задания на практики по курсу "Сложность пропозициональных доказательств"

Домашние задания на очередное практическое занятие появляются на странице этого занятия. Например, задание на занятие 19-го сентября следует искать тут.