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

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

В докладе для любой цейтинской невыполнимой формулы на графе 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 будет отправлена за пару часов до доклада.

Proving super-logarithmic data structure lower bounds in the static group model has been a fundamental challenge in computational geometry since the early 80's. We prove a polynomial ($n^{\Omega(1)}$) lower bound for an explicit range counting problem of $n^3$ convex polygons in $\R^2$ (each with $n^{\tilde{O}(1)}$ facets/semialgebraic-complexity), against linear storage arithmetic data structures in the group model. Our construction and analysis are based on a combination of techniques in Diophantine approximation, pseudorandomness, and compressed sensing---in particular, on the existence and partial derandomization of optimal \emph{binary} compressed sensing matrices in the polynomial sparsity regime ($k = n^{1-\delta}$). As a byproduct, this establishes a (logarithmic) separation between compressed sensing matrices and the stronger RIP property.