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.***

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