Home

Понедельник 19.11. Федор Парт: "Нижние оценки для резолюций с линейными уравнениями над кольцами"

Понедельник, 19 ноября, ауд. 106. Начало в 14:00.

Докладчик: Федор Парт.

Тема: Нижние оценки для резолюций с линейными уравнениями над кольцами.

Abstract

Система доказательств Res($ lin_R $) определяется как расширение резолюционной системы доказательств Res, в ней выводимыми утверждениями являются дизъюнкции линейных уравнений над кольцом R. Одна из мотиваций для изучения таких систем заключается в том, что если R - это конечное поле $ F_p $ или поле рациональных чисел, то Res(lin_R) является простейшим примером систем $ AC_0[p] $-Frege или $ TC_0 $-Frege соответственно, доказательство суперполиномиальных нижних оценок на длины доказательств в которых - давно открытая проблема. Оказывается, даже для Res($ lin_R $) проблема доказательства нижних оценок в общем случае крайне нетривиальна и на данный момент является открытой.

В докладе мы докажем ряд dag-like и tree-like верхних и нижних оценок на размер доказательств в Res($ lin_F $) для разных полей F. В случае char(F)=0 мы докажем экпоненциальную нижнюю оценку, но не для КНФ, а для клоза вида $ a_1x_1+...+a_nx_n=A $ для больших, то есть растущих суперполиномиально от n, коэффициентов. Эта оценка получается как следствие из полиномиальных нижних и верхних оценок на размер кратчайшего Res($ lin_F $) доказательства как функции от размера образа линейной формы $ a_1x_1+...+a_nx_n $. Также в случае char(F)=0 мы докажем экспоненциальную tree-like нижнюю оценку на $ a_1x_1+...+a_nx_n=A $, если коэффициенты малы, то есть ограничены полиномом от 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} $) нижней оценки на PHP для произольных полей F с помощью теоремы Алона-Фюреди о покрытиях гиперкуба гиперплоскостями.

Доклад основан на совместной статье с И. Цамеретом.