В теории сложности доказательств часто рассматривается такая задача поиска: дана невыполнимая формула в КНФ и набор значений ее переменных, требуется найти дизъюнкт формулы, который опровергается этим значением переменных. Известно, что доказательство невыполнимости формулы во многих древовидных системах доказательств можно перестроить в вероятностный коммуникационный протокол для этой задачи поиска. Тем самым для доказательства нижней оценки на сложность древовидного вывода достаточно доказать нижнюю оценку на коммуникационную задачу. Мы будем рассматривать вероятностную коммуникационную сложность для двух участников и k участников в модели "число на лбу".

Первую нижнюю оценку на вероятностную коммуникационную сложность задач поиска получили Бим, Питасси и Сегерлинд (2007), затем Гёс и Питасси (2013) получили более простое доказательства нижней оценки на коммуникационную сложность задачи поиска через его критическую блочную чувствительность. Оба этих результата использую искусственные формулы: в традиционную формулу добавляется гаджет, то есть каждая переменная в формуле заменяется на функцию от свежих переменных, значения которых разделяются между участниками коммуникационного протокола. Мы предлагаем новый способ доказательства нижних оценок на коммуникационную сложность задач поиска, который позволяет получать нижние оценки на естественные формулы.
Таким образом, мы доказываем:
* Точную экспоненциальную нижнюю оценку на сложность опровержения принципа совершенного паросочетания для полного двудольного графа в системе Res($\oplus$).
* Экспоненциальную нижнюю оценку на сложность бинарного принципа Дирихле для древовидных систем, оперирующих строками доказательств, которые можно вычислить с небольшой вероятностной коммуникацией.

Доклад основан на совместной работе с Д. Ицыксоном.

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