Laboratory of Mathematical Logic at PDMI

Пятница, 23 ноября, ауд. 106. Начало в 14:00.

Докладчик: Анастасия Софронова.

Тема: Верхние оценки на размер dag-like коммуникационных протоколов.

Abstract

Dag-like коммуникационные протоколы — обобщение классических коммуникационных протоколов. С их помощью можно перенести нижние оценки на ширину резолюционного доказательства невыполнимой формулы на другие системы доказательств, а также на размер монотонных схем для некоторых связанных задач. Для этого используется техника lifting — вместо каждой переменной формулы подставляется некоторая функция от новых переменных, так называемый гаджет. Однако известные гаджеты, подходящие для этой техники, имеют большой размер. Вопрос, можно ли использовать гаджет константного размера, является открытым. Мы рассмотрим некоторые конкретные гаджеты константного размера и приведём пример семейства формул, показывающий, что их нельзя использовать для переноса нижних оценок. А именно, рассмотрим семейство формул с минимальной шириной резолюционного доказательств и полиномиальным размером dag-like протокола для задачи поиска невыполненного дизъюнкта после подстановки гаджета.