Оптимальные системы доказательств и алгоритмы (обзор)

Оптимальная система доказательств — система, доказательства в которой не более, чем в полиномиальное количество раз длиннее, чем в любой другой системе. Если к тому же доказательства могут быть переделаны из доказательств в другой системе за полиномиальное время, система называется $p$-оптимальной.
Существование ($p$-)оптимальной системы доказательств для языка пропозициональных тавтологий (и многих других языков) является важным открытым вопросом теории сложности. Я. Крайичек и П. Пудлак (1989) показали связь этого вопроса с существованием оптимальной полуразрешающей процедуры для этого языка. Недавно Х. Монро (2009) доказал отсутствие такой процедуры при некоторых дополнительных предположениях.
В последние годы отсутствие эффективной перечислимости (а значит, и подобного рода универсальных объектов) преодолевалось либо переходом к эвристическим вычислениям (когда имеется вероятностное распределение на входах и допустима ошибка с небольшой вероятностью), либо использованием небольшого количества битов неравномерной подсказки (единой для всех входов одной длины). В частности, С. Кук и Я. Крайичек (2007) показали наличие $p$-оптимальной системы доказательств с неравномерной подсказкой; докладчиком же (совместно с Д. М. Ицыксоном) получена оптимальная полуразрешающая эвристическая процедура для любого полиномиально моделируемого распределения, заданного на дополнении языка.