Резолюция является наиболее хорошо изученной системой доказательств. Известные техники для доказательств нижних оценок на данную систему плохо применимы в случае, когда формула <<перегружена>> переменными. Одним из ярких примеров <<нехорошей>> для резолюций формулы является Weak-PigeonHole (принцип Дирихле с m кроликами и n клетками, причем m >> n^2). Впервые нижняя оценка для данной формулы была доказана Разом в 2001 году, Разборов впоследствии усилил и обобщил с помощью своего так называемого метода псевдоширины.

На семинаре мы обсудим технику псевдо-ширины, и покажем нижнюю оценку на weak-PHP для разреженных графов. Совместная работа с Susanna F. de Rezende, Jakob Nordström и Kilian Risse.

Система доказательств Res(+), предложенная Ицыксоном и Соколовым, -- расширение резолюционной системы доказательств. Она оперирует с дизъюнкциями линейных равенств над $F_2$. В докладе мы рассмотрим технику доказательства нижних оценок на размер доказательств некоторых противоречивых семейств формул для древовидной Res(+), основанную на играх Прувера и Дилеера. Данная техника является обобщением доказательства нижней оценки для принципа Дирихле. Затем мы применим данную технику для доказательства нижних оценок на Ordering principle и Dense Linear Ordering principle.

Ordering principle утверждает, что не существует конечного линейного порядка без минимума. Мы дадим нижнюю оценку $2^{n−O(1)}$ на размер любого древовидного Res(+) доказательства этого утверждения, записанного в КНФ. Dense Linear Ordering principle утверждает, что не существует конечных плотных линейных порядков. Мы дадим $2^{n/3−O(1)}$ нижнюю оценку на размер любого древовидного Res(+) доказательства этого утверждения, записанного в КНФ.

Ordering principle и Dense Linear Ordering principle имеют доказательство полиномиального размера в резолюциях. Таким образом, мы приведем естественные примеры, разделяющие древовидную версию системы Res(+) и резолюцию.

Упорядоченные диаграммы принятия решений (OBDD) - это частный случай однопроходных ветвящихся программ, в которых переменные встречаются в определенном порядке. Наложенное ограничение позволяет эффективно выполнять многие операции с булевыми функциями, записанными в этом виде. В 2004 году Атсериас, Варди и Колайтис предложили систему доказательств, в которых строки доказательств записываются в виде OBDD, из двух OBDD можно выводить любую OBDD, которая из них семантически следует. В 2008 году Крайчек доказал экспоненциальную нижнюю оценку в этой системе доказательств, если все OBDD в доказательстве используют одни и те же порядки на переменных. Если разрешить использовать в доказательствах OBDD в разных порядках, то получится строго более сильная система доказательств, для которой суперполиномиальных нижних оценок не известно.

В докладе мы рассмотрим исчисление однопроходных ветвящихся программ (1-BP), в котором можно выводить новые 1-BP как конъюнкцию уже имеющихся или как проекцию имеющейся 1-BP. Это семантическое обобщение некоторой подсистемы упомянутой выше OBDD-системы доказательств, в которой можно использовать различные порядки на переменных в OBDD. Мы покажем, что существует семейство невыполнимых формул $F_n$ в O(1)-КНФ и константа C, что любой вывод в этом исчислении, использующий проекции по не более, чем Cn различным переменным, имеет размер хотя бы $2^{\Omega(n)}$.

Доклад основан на совместной работе с С. Басом, А. Кнопом, А. Рязановым и Д. Соколовым.