Home

Семинар 3 декабря 2004 года

Пятница, 3 декабря, комната 106. Начало в 17:30.

Докладчик: С. И. Николенко.

Тема: Cutting Plane с ограниченной избыточностью.

Abstract

Речь пойдет об ослабленных вариантах системы доказательств Cutting Plane; именно, ``избыточность'' промежуточных неравенств ограничивается некоторой функцией (``избыточность'' --- количество литералов, которые можно удовлетворить, не делая неравенство тривиальным). В отличие от системы Cutting Plane без ограничений, для таких систем доказана суперполиномиальная нижняя оценка на длину вывода цейтинских тавтологий: Гердт доказал это вплоть до избыточности $ n / log^2 n $.

В докладе будет показано, как несложно промоделировать такие доказательства резолюционными. Тем самым оценка Гердта улучшается до $ o(n / log n) $. Кроме того, есть шанс, что этот метод может привести к более сильным результатам.

Результаты получены совместно с Э.А.Гиршем.