Нижние оценки на длину вывода цейтинских формул в статической системе доказательств Ловаса–Схрайвера

Статья посвящена графам-расширителям и их использованию в теории сложности алгоритмов и доказательств. Мы обобщаем с матриц на графы результат Алехновича и Разборова, состоящий в том, что при выкидывании достаточно малого линейного относительно количества вершин числа любых ребер возможно сохранить расширяющие свойства графа. Воспользовавшись этим свойством, мы даем ответ на поставленный Григорьевым и др. вопрос о нижней экспоненциальной оценке на размер вывода булевых формул в ДНФ для статических полуалгебраических систем доказательств. Ранее для этих систем доказательств была известна нижняя оценка для системы неравенств “симметричный рюкзак”, которая не имеет короткой записи в виде булевой формулы. Мы показываем, что размер любого доказательства в статической системе доказательств Ловаса–Схрайвера ($LS_+$) цейтинских формул имеет не менее чем экспоненциальный размер. Следствием является нижняя экспоненциальная оценка на размер древовидного доказательства в $LS_+$. Библ. – 22 назв.