City: Санкт-Петербург Новосибирск Казань Language: Русский English

Propositional proof complexity
Новосибирск / autumn 2019, посмотреть все семестры

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. Основная программа исследований в теории сложности доказательств заключается в доказательстве суперполиномиальных нижних оценок для как можно более мощных систем доказательств.

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

Date and time Class|Name Venue|short Materials
17 October
16:20–17:55
Лекция 1, lecture НГУ, ауд. 4117 videocourseclass|other [materials]
17 October
18:10–19:45
Лекция 2, lecture НГУ, ауд. 4117 videocourseclass|other [materials]
18 October
16:20–17:55
Лекция 3, lecture НГУ, ауд. 4117 videocourseclass|other [materials]
18 October
18:10–19:45
Лекция 4, lecture НГУ, ауд. 4117 videocourseclass|other [materials]
19 October
16:20–17:55
Лекция 5, lecture НГУ, ауд. 4117 videocourseclass|other [materials]
19 October
18:10–19:45
Лекция 6, lecture НГУ, ауд. 4117 videocourseclass|other [materials]