Laboratory of Mathematical Logic at PDMI

Пятница, 2 октября, Zoom. Начало в 18:00.

Докладчик: Пётр Смирнов.

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

Abstract

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