Seminars

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



Понедельник 11.10. А.В. Смаль (ПОМИ РАН): "Доказательство нижних оценок на размер формул для булевых функций методами коммуникационной сложности"

Speaker: 
А.В. Смаль (ПОМИ РАН)
Date: 
Monday, October 11, 2021 - 11:00
Place: 
Zoom
Abstract: 

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

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

Далее будет рассказано о гипотезе Карчмера - Раза - Вигдерсона и её варианте для композиции с мультиплексером. При рассмотрении этой задачи естественным образом возникает необходимость рассмотреть альтернативную модель вычисления для коммуникационной сложности. В качестве такой модели будет предложена концепция полудуплексной коммуникационной сложности и рассказано о результатах в этой области.

В заключение будет рассказано о том, как с использованием полудуплексной коммуникационной сложности получить нетривиальную нижнюю оценку на композицию универсального отношения и некоторой функции.



Суббота 09.10. Petr Smirnov (HSE - SPb): "Regular resolution lower bounds for Tseitin formulas via treewidth"

Speaker: 
Petr Smirnov (HSE - SPb)
Date: 
Saturday, October 9, 2021 - 11:00
Place: 
Zoom
Abstract: 

In this talk, we will discuss some bounds for regular resolution refutations of unsatisfiable Tseitin formulas. These bounds estimate the size of a proof via treewidth of the underlying graph.

Reducing the lower bounds for unsatisfiable formulas to the lower bounds for the satisfiable case and obtaining such bounds, we got the lower bound exp(Ω(tw(G) / log(V))) in [1].
Recently, de Colnet and Mengel [2] got the lower bound exp(Ω(tw(G) / Δ(G))) (up to polynomial factor) using the similar reduction concept. There is a known upper bound exp(O(tw(G) * Δ(G))), so the bound is tight for constant-degree graphs.

However, the question for all graphs is still open. Also, there are two lower bounds, and while the latter bound is stronger for graphs of small degrees, the former is better for graphs of large degrees.

Now we've got the new lower bound exp(Ω(tw(G))) (up to polynomial factor). It is stronger than both of the previous bounds and bring us closer to the tight bound for all Tseitin formulas.

[1] Itsykson D., Riazanov A., Sagunov D., Smirnov P. Near-Optimal Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs. Comput. Complex. 30, 13 (2021).
[2] de Colnet A., Mengel S. (2021) Characterizing Tseitin-Formulas with Short Regular Resolution Refutations. In Proceedings of SAT 2021.



Пятница 26.03. Marc Vinyals (Technion): "The power of restarts in CDCL solvers"

Speaker: 
Marc Vinyals (Technion)
Date: 
Friday, March 26, 2021 - 11:30
Place: 
ZOOM
Abstract: 

The CDCL algorithm -- or DPLL extended with clause learning -- is allowed to forget its position in the search space and restart from the root of the search tree. This restart operation seems useful both in theory and in practice, but so far we have not been able to pin down whether it is really needed and why.

At the same time, most of the analysis of CDCL has been done with unsatisfiable formulas as inputs, simply because in the usual models of CDCL all satisfiable formulas are trivially easy. In order to obtain meaningful one has to use more exotic models such as the "drunk" model where the first branch of the search tree to visit is picked randomly.

In this talk we combine these two topics, restarts and satisfiable inputs, and show that in the drunk model of CDCL there exist satisfiable formulas such that using restarts gives an exponential speedup over not using restarts.

***This is the joint session with the informal Proof Complexity seminar. Attention: the duration of the talk may be up to 3 hours! The zoom link will be sent to the seminar mail list before the talk.***



Среда 07.10. Анастасия Софронова: "Нижние оценки на задачи поиска для (1, +k)-ветвящихся программ"

Speaker: 
Анастасия Софронова
Date: 
Wednesday, October 7, 2020 - 18:00
Place: 
Zoom (обратите внимание на нестандартный день семинара!)
Abstract: 

В докладе мы докажем нижнюю оценку на задачу поиска невыполненного клоза для ветвящихся программ с ограниченным числом повторений переменных; а именно, нижнюю оценку $2^\Omega(n/k^2)$ для семейства формул $f_n$ размера poly(n) и $k = O(\log n/ \log \log n)$, где k — число повторений переменных. Семейство формул представляет собой некоторую модификацию невыполнимых формул, кодирующих существование линейного порядка без минимума на множестве из n элементов.

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



Пятница 02.10. Пётр Смирнов: "Квазиполиномиальные опровержения цейтинских формул в Cutting Planes"

Speaker: 
Пётр Смирнов
Date: 
Friday, October 2, 2020 - 18:00
Place: 
Zoom
Abstract: 

В докладе для любой цейтинской невыполнимой формулы на графе G мы построим опровержение в системе Cutting Planes (CP) длины $2^D (nD)^O(log n)$, где n — число вершин графа G, а D — его максимальная степень.

Опровержение строится следующим образом: мы рассматриваем (построенное ранее в другой работе) квазиполиномиальное опровержение в более сильной системе Stabbing Planes, замечаем структурное свойство этого опровержения, а затем перестраиваем любое опроверждение с таким свойством в систему CP.

Таким образом, этим результатом была опровергнута гипотеза о том, что цейтинские формулы экспоненциально сложны для CP.

Доклад основан на статье Daniel Dadush и Samarth Tiwari «On the Complexity of Branching Proofs» [https://homepages.cwi.nl/~dadush/papers/branching.pdf].

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


Pages