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