Понедельник, 19 ноября, ауд. 106. Начало в 14:00.
Докладчик: Федор Парт.
Тема: Нижние оценки для резолюций с линейными уравнениями над кольцами.
Abstract
Система доказательств Res(
![$ lin_R $](../../../sites/default/files/tex/f8d7737ec01b30cb4e409eec61f3b1727b6747ed/index.png)
) определяется как расширение резолюционной системы доказательств Res, в ней выводимыми утверждениями являются дизъюнкции линейных уравнений над кольцом R. Одна из мотиваций для изучения таких систем заключается в том, что если R - это конечное поле
![$ F_p $](../../../sites/default/files/tex/a484aa71e2137f9f62aba2b677f9da2f0b0279b3/index.png)
или поле рациональных чисел, то Res(lin_R) является простейшим примером систем
![$ AC_0[p] $](../../../sites/default/files/tex/6ca5b9ac10ef294dc75757307886553be3f465ea/index.png)
-Frege или
![$ TC_0 $](../../../sites/default/files/tex/38f8bd0becbebe133a77465707f091cd868318a0/index.png)
-Frege соответственно, доказательство суперполиномиальных нижних оценок на длины доказательств в которых - давно открытая проблема. Оказывается, даже для Res(
![$ lin_R $](../../../sites/default/files/tex/f8d7737ec01b30cb4e409eec61f3b1727b6747ed/index.png)
) проблема доказательства нижних оценок в общем случае крайне нетривиальна и на данный момент является открытой.
В докладе мы докажем ряд dag-like и tree-like верхних и нижних оценок на размер доказательств в Res(
![$ lin_F $](../../../sites/default/files/tex/556dcd42d0bfa3ddadabbdfa9283e82709ee913f/index.png)
) для разных полей F. В случае char(F)=0 мы докажем экпоненциальную нижнюю оценку, но не для КНФ, а для клоза вида
![$ a_1x_1+...+a_nx_n=A $](../../../sites/default/files/tex/eb5095da35c1a9a07ce1d0f127e05fc4ec13ca82/index.png)
для больших, то есть растущих суперполиномиально от n, коэффициентов. Эта оценка получается как следствие из полиномиальных нижних и верхних оценок на размер кратчайшего Res(
![$ lin_F $](../../../sites/default/files/tex/556dcd42d0bfa3ddadabbdfa9283e82709ee913f/index.png)
) доказательства как функции от размера образа линейной формы
![$ a_1x_1+...+a_nx_n $](../../../sites/default/files/tex/042f7bdbcc701dac8ddbd6eecee0548ada20e622/index.png)
. Также в случае char(F)=0 мы докажем экспоненциальную tree-like нижнюю оценку на
![$ a_1x_1+...+a_nx_n=A $](../../../sites/default/files/tex/eb5095da35c1a9a07ce1d0f127e05fc4ec13ca82/index.png)
, если коэффициенты малы, то есть ограничены полиномом от n. Это влечет экспоненциальное разделение dag-like и tree-like Res(lin_F) в случае малых коэффициентов
Для конечных полей мы докажем экспоненциальные разделения между tree-like Res(lin_Fp) и tree-like Res(lin_Fq) для различных p и q, где в качестве разделяющих КНФ использованы mod-p Цейтинские формулы. Этот результат, а также экспоненциальная нижняя оценка для tree-like Res(lin_Fp) на случайных КНФ, получается как следствие варианта классического соотношения ширины и размера резолюционных доказательств вкупе с нижней оценкой на ширину через симуляцию в Polynomial Calculus. Мы обобщим доказательство Ицыксона и Соколова tree-like Res(
![$ lin_{F_2} $](../../../sites/default/files/tex/3b6f93641bb4593f4a3f5c95f9dde4c0a6f73f3c/index.png)
) нижней оценки на PHP для произольных полей F с помощью теоремы Алона-Фюреди о покрытиях гиперкуба гиперплоскостями.
Доклад основан на совместной статье с И. Цамеретом.