Seminars

Mailing list: https://groups.google.com/forum/#!forum/spb-algo



Пятница 07.08. Ярослав Алексеев (СПбГУ): "Нижняя оценка для обобщения системы PC и моделирование системы Res-Lin"

Speaker: 
Ярослав Алексеев (СПбГУ)
Date: 
Friday, August 7, 2020 - 11:00
Place: 
Zoom
Abstract: 

Мы рассмотрим обобщение системы Polynomial Calculus, в котором дополнительно можно извлекать квадратный корень из многочлена и вводить новые переменные, записывающие многочлены от исходных переменных. Мы докажем экспоненциальную нижнюю оценку на размер опровержения в этой системе равенства $BVP_n$ ($1 + 2 x_1 + 2^2 x_2 + ... + 2^n x_n = 0$), при этом для доказательства нижней оценки на размер доказательства нам не потребуется нижняя оценка на степень. Благодаря тому, что эта система полиномиально моделирует Res-Lin (систему, оперирующую дизъюнкциями линейных уравнений; введена Разом и Цамеретом), мы получим альтернативное доказательство нижней оценки Парта и Цамерета на размер доказательств $BVP_n$ в Res-Lin.

Семинар будет проходить онлайн в конференции zoom. Ссылка для подключения будет выслана в рассылку за пару часов до доклада.



Пятница 31.07. Виталий Демьянюк: "Теоретические оценки качества и сложности алгоритмов в дизайне сетевых элементов"

Speaker: 
Виталий Демьянюк
Date: 
Friday, July 31, 2020 - 17:00
Place: 
Конференция Zoom
Abstract: 

В современных сетях число пользователей растет экспоненциально, структура сети становится все более сложной, а количество поддерживаемых стандартов постоянно увеличивается. Все это приводит к тому, что состояние сети становится сложным по структуре. С другой стороны, требования эффективности тоже быстро растут (обработка одного пакета должна происходить на уровне десятков или сотен наносекунд). В результате нужно искать компромисс между выразительностью представления состояния сети и эффективностью обработки пакетов. В первой части мы рассмотрим три проекта, посвящённых эффективному представлению программ, обрабатывающих пакеты. Во второй части мы покажем, как можно использовать ресурсы всей сети для задачи мониторинга трафика, уменьшающего локальный размер состояния в каждом отдельном элементе.

Семинар будет проходить онлайн в конференции zoom. Ссылка для подключения будет выслана в рассылку за пару часов до доклада.



Пятница 05.06. Дмитрий Соколов (СПбГУ, ПОМИ): "Нижние оценки на систему AC_0-Frege"

Speaker: 
Дмитрий Соколов (СПбГУ, ПОМИ)
Date: 
Friday, June 5, 2020 - 16:00
Place: 
Zoom
Abstract: 

В этом докладе мы обсудим детали доказательства нижней оценки на систему доказательств AC_0-Frege. Нашей основной целью будет разобраться в технических деталях switching леммы для паросочетаний из классической статьи Urquhart, Fu ``Simplified Lower Bounds for Propositional Proofs''.



Пятница 29.05. Артур Рязанов (ПОМИ РАН): "Нижние оценки на коммуникационную сложность задач поиска с гаджетом четности и без гаджета"

Speaker: 
Артур Рязанов (ПОМИ РАН)
Date: 
Friday, May 29, 2020 - 18:10
Place: 
Zoom
Abstract: 

В теории сложности доказательств часто рассматривается такая задача поиска: дана невыполнимая формула в КНФ и набор значений ее переменных, требуется найти дизъюнкт формулы, который опровергается этим значением переменных. Известно, что доказательство невыполнимости формулы во многих древовидных системах доказательств можно перестроить в вероятностный коммуникационный протокол для этой задачи поиска. Тем самым для доказательства нижней оценки на сложность древовидного вывода достаточно доказать нижнюю оценку на коммуникационную задачу. Мы будем рассматривать вероятностную коммуникационную сложность для двух участников и k участников в модели "число на лбу".

Первую нижнюю оценку на вероятностную коммуникационную сложность задач поиска получили Бим, Питасси и Сегерлинд (2007), затем Гёс и Питасси (2013) получили более простое доказательства нижней оценки на коммуникационную сложность задачи поиска через его критическую блочную чувствительность. Оба этих результата использую искусственные формулы: в традиционную формулу добавляется гаджет, то есть каждая переменная в формуле заменяется на функцию от свежих переменных, значения которых разделяются между участниками коммуникационного протокола. Мы предлагаем новый способ доказательства нижних оценок на коммуникационную сложность задач поиска, который позволяет получать нижние оценки на естественные формулы.
Таким образом, мы доказываем:
* Точную экспоненциальную нижнюю оценку на сложность опровержения принципа совершенного паросочетания для полного двудольного графа в системе Res($\oplus$).
* Экспоненциальную нижнюю оценку на сложность бинарного принципа Дирихле для древовидных систем, оперирующих строками доказательств, которые можно вычислить с небольшой вероятностной коммуникацией.

Доклад основан на совместной работе с Д. Ицыксоном.

Ссылка на конференцию Zoom будет выслана на рассылку семинара за несколько часов до доклада.



Пятница 22.05. Артур Рязанов (ПОМИ РАН): "Применение критерия Юкны для нижних оценок в системе доказательств Cutting Planes"

Speaker: 
Артур Рязанов (ПОМИ РАН)
Date: 
Friday, May 22, 2020 - 18:10
Place: 
Zoom
Abstract: 

Это продолжение предыдущего доклада. Мы рассмотрим взвешенный критерий Стасиса Юкны для доказательства нижних оценок на монотонную вещественную схемную сложность. Затем мы покажем, как его применить для доказательства экспоненциальной нижней оценки на сложность опровержения бинарного принципа Дирихле в системе доказательств Cutting Planes (результат Павла Пудлака и Павла Грубеша).

Ссылка на конференцию Zoom будет отправлена на рассылку семинара за несколько часов до доклада.


Pages