Введение

В теории сложности теорема Карпа-Липтона гласит, что если булевую задачу удовлетворимости (SAT) можно решить булевыми цепями с полиномиальным числом логических ворот, то и следовательно, если мы предположим, что NP, класс недетерминированных многочленных задач во времени, может содержаться в неравномерном полиномиальном классе сложности времени P/poly, то это предположение подразумевает крах многочленной иерархии на втором уровне. Такой коллапс считается маловероятным, поэтому теорему обычно рассматривают теоретики сложности как доказательство несуществования цепей многочленного размера для SAT или для других NP-полных задач. Доказательство того, что таких цепей не существует, будет означать, что P ≠ NP. Поскольку P/poly содержит все проблемы, разрешимые в рандомизированном полиномиальном времени (теорема Адлемана), теорема также является доказательством того, что использование рандомизации не приводит к алгоритмам в полиномиальном времени для NP-полных проблем. Теорема Карпа-Липтона названа в честь Ричарда М. Карпа и Ричарда Дж. Липтона, которые впервые доказали ее в 1980 году. (Их первоначальное доказательство упало до PH , но Майкл Сипсер улучшил его до .) Варианты теоремы утверждают, что при том же предположении MA = AM, и PH переходит в класс сложности. Более убедительные выводы возможны, если предполагается, что PSPACE или некоторые другие классы сложности имеют схемы многочленного размера; см. P/poly. Если NP считается подмножеством BPP (которое является подмножеством P/poly), то иерархия полиномов сворачивается до BPP. Если coNP считается подмножеством NP/поли, то иерархия полиномов падает до третьего уровня.

Интуиция

Предположим, что схемы многочленного размера для SAT не только существуют, но и могут быть построены алгоритмом многочленного времени. Тогда это предположение подразумевает, что сам SAT может быть решен алгоритмом многочленного времени, который строит схему, а затем применяет ее. То есть эффективно строимые схемы для SAT приведут к более сильному коллапсу, P = NP. Предположение теоремы Карпа-Липтона, что эти цепи существуют, является более слабым. Но все же возможно, чтобы алгоритм в классе сложности угадал правильную схему для SAT. Класс сложности описывает задачи формы, где любой полиномиальный срок является вычислимым предикатом. Экзистенциальная мощность первого количественного показателя в этом предикате может быть использована для угадывания правильной схемы для SAT, а универсальная мощность второго количественного показателя может быть использована для проверки правильности схемы. После того, как эта схема будет угадана и проверена, алгоритм в классе может использовать ее в качестве подпрограммы для решения других задач.

Доказательство теоремы Карпа Липтона

Теорема Карпа-Липтона может быть переформулирована в результате булевых формул с полиномиально ограниченными количественными знаками. Проблемы в описываются формулами такого типа, с синтаксисом где является многочленное время вычислимое предикат. Теорема Карпа-Липтона гласит, что этот тип формулы может быть преобразован в полиномиальное время в эквивалентную формулу, в которой количественники появляются в противоположном порядке; такая формула относится к Обратите внимание, что подформула является примером SAT. То есть, если c является действительной схемой для SAT, то эта подформула эквивалентна неквантифицированной формуле c ((s ((x)). Поэтому полная формула для эквивалентна (при предположении, что существует действительная схема с) формуле, где V - это формула, используемая для проверки того, что c действительно является действительной схемой с использованием саморедуктивности, как описано выше. Эта эквивалентная формула имеет свои количественные показатели в обратном порядке, как желательно. Поэтому предположение Карпа-Липтона позволяет нам перенести порядок экзистенциальных и универсальных квантификаторов в формулы такого типа, показывая, что повторение переноса позволяет формулам с более глубоким вложенным объединением упростить формулу, в которой они имеют один экзистенциальный квантификатор, за которым следует один универсальный квантификатор, показывая, что