City: Saint Petersburg Novosibirsk Kazan Language: Русский English

Propositional proof complexity
Saint Petersburg / autumn 2017, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

Дана система линейных нестрогих неравенств с целыми коэффициентами. Чтобы доказать, что эта система имеет вещественное решение, можно просто его предъявить. А как доказать, что система несовместна? Это сделать можно, например, с помощью леммы Фаркаша, которая утверждает, что если система нестрогих линейных неравенств несовместна, то можно сложить эти неравенства с неотрицательными коэффициентами и получить противоречивое неравенство \(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-пара системы доказательств
    • Оптимальные системы доказательств и оптимальный алгоритм
    • Автоматизируемость (поиск доказательств)

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

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

Вопросы к экзамену:

Date and time Class|Name Venue|short Materials
12 September
18:30–20:00
Лекция 1. Деревья решений, Lecture ПОМИ РАН other
12 September
20:20–21:50
Практика 1., Seminar ПОМИ РАН files
19 September
18:30–20:00
Лекция 2. Метод резолюций, Lecture ПОМИ РАН No
19 September
20:20–21:50
Практика 2., Seminar ПОМИ РАН files
26 September
18:30–20:00
Лекция 3. Ширина и размер резолюционных доказательств, Lecture ПОМИ РАН No
26 September
20:20–21:50
Практика 3., Seminar ПОМИ РАН files
03 October
18:30–20:00
Лекция 4. Игровая интерепретация ширины, Lecture ПОМИ РАН No
03 October
20:20–21:50
Практика 4, Seminar ПОМИ РАН files
10 October
18:30–20:00
Лекция 5. CDCL алгоритмы, Lecture ПОМИ РАН No
10 October
20:20–21:50
Практика 5, Seminar ПОМИ РАН files
17 October
18:30–20:00
Лекция 6. Исчисление полиномов, Lecture ПОМИ РАН No
17 October
20:20–21:50
Практика 6., Seminar ПОМИ РАН files
24 October
18:30–20:00
Лекция 7. Нижние оценки для исчисления полиномов, Lecture ПОМИ РАН No
24 October
20:20–21:50
Практика 7., Seminar ПОМИ РАН files
31 October
18:30–20:00
Лекция 8. Секущие плоскости, Lecture ПОМИ РАН No
31 October
20:20–21:50
Практика 8., Seminar ПОМИ РАН files
07 November
18:30–20:00
Лекция 9. Монотонная интерполяция, Lecture ПОМИ РАН No
07 November
20:20–21:50
Практика 9., Seminar ПОМИ РАН files
14 November
18:30–20:00
Лекция 10. Древовидные системы доказательств и вероятностная коммуникация, Lecture ПОМИ РАН No
14 November
20:20–21:50
Практика 10., Seminar ПОМИ РАН files
21 November
18:30–20:00
Лекция 11. Коммуникационная сложность и критическая блочная чувствительность, Lecture ПОМИ РАН No
21 November
20:20–21:50
Практика 11, Seminar ПОМИ РАН files
28 November
18:30–20:00
Лекция 12. Системы Фреге, Lecture ПОМИ РАН No
28 November
20:20–21:50
Практика 12, Seminar ПОМИ РАН files
05 December
18:30–20:00
Лекция 13. Нижняя оценка для систем Фреге константной глубины, Lecture ПОМИ РАН No
05 December
20:20–21:50
Практика 13., Seminar ПОМИ РАН files
12 December
18:30–20:00
Лекция 14. Нижняя оценка в системах Фреге ограниченной глубины (продолжение), Lecture ПОМИ РАН No
12 December
20:20–21:50
Практика 14, Seminar ПОМИ РАН files
19 December
18:30–20:00
Лекция 15. Оптимальные и p-оптимальные системы доказательств, Lecture ПОМИ РАН No
19 December
20:20–21:50
Практика 15, Seminar ПОМИ РАН No