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