Сложность доказательства

редактировать

В теоретической информатике и, в частности, в теории сложности вычислений, доказательство сложность - это область, направленная на понимание и анализ вычислительных ресурсов, необходимых для подтверждения или опровержения утверждений. Исследования сложности доказательства в основном связаны с доказательством нижних и верхних оценок длины доказательства в различных пропозициональных системах доказательства. Например, одна из основных проблем сложности доказательства - показать, что система Фреге, обычное исчисление высказываний, не допускает доказательств полиномиального размера для всех тавтологий; здесь размер доказательства - это просто количество символов в нем, и доказательство называется полиномиальным размером, если оно полиномиально по размеру тавтологии, которую оно доказывает.

Систематическое изучение сложности доказательства началось с работы Стивена Кука и (1979), который дал базовое определение пропозициональной системы доказательства с точки зрения вычислительной сложности. В частности, Кук и Реккау отметили, что доказательство нижних границ размера доказательства для более сильных и сильных пропозициональных систем доказательства можно рассматривать как шаг к отделению NP от coNP (и, таким образом, P от NP), поскольку существование пропозициональной системы доказательств, допускающей доказательства полиномиального размера для всех тавтологий, эквивалентно NP = coNP.

Современные исследования сложности доказательств привлекают идеи и методы из многих областей вычислительной сложности, алгоритмов и математики. Поскольку многие важные алгоритмы и алгоритмические методы могут быть использованы как алгоритмы поиска доказательств для определенных систем доказательства, доказательство нижних границ размеров доказательств в этих системах подразумевает нижние границы времени выполнения для соответствующих алгоритмов. Это связывает сложность доказательства с более прикладными областями, такими как решение SAT.

Математическая логика также может служить основой для изучения размеров пропозициональных доказательств. Теории первого порядка и, в частности, слабые фрагменты Арифметики Пеано, которые имеют название теории ограниченной арифметики, служат единообразными версиями систем пропозициональных доказательств и обеспечивают дальнейшую основу для интерпретации короткие пропозициональные доказательства с точки зрения различных уровней допустимых рассуждений.

Содержание

1 Системы доказательства
2 Доказательства размера полинома и проблема NP и coNP
3 Оптимальность и моделирование между системами доказательства
4 Автоматизация поиска доказательства
5 Ограниченная арифметика
6 SAT-решатели
7 Нижние границы
8 Возможная интерполяция
9 Неклассическая логика
10 См. Также
11 Ссылки
12 Дополнительная литература
13 Внешние ссылки

Системы доказательств

Система пропозициональных доказательств дается как алгоритм проверки-доказательства P (A, x) с двумя входами. Если P принимает пару (A, x), мы говорим, что x является P-доказательством A. P требуется для выполнения за полиномиальное время, и, более того, должно выполняться, что A имеет P-доказательство тогда и только тогда, когда оно тавтология.

Примеры пропозициональных систем доказательства включают последовательное исчисление, разрешение, плоскости разделения и систему Фреге. Сильные математические теории, такие как ZFC, также порождают системы пропозициональных доказательств: доказательство тавтологии $τ {\ displaystyle \ tau}$ $\ тау$ в пропозициональной интерпретации ZFC - это ZFC- доказательство формализованного утверждения « $τ {\ displaystyle \ tau}$ $\ тау$ является тавтологией».

Доказательства полиномиального размера и проблема NP и coNP

Сложность доказательства измеряет эффективность системы доказательств обычно с точки зрения минимального размера доказательств, возможных в системе для данной тавтологии. Размер доказательства (соотв. Формулы) - это количество символов, необходимых для представления доказательства (соотв. Формулы). Система пропозициональных доказательств P полиномиально ограничена, если существует константа $c {\ displaystyle c}$ $c$ такая, что каждая тавтология размера $n {\ displaystyle n}$ $n$ имеет P-proof размера $(n + c) c {\ displaystyle (n + c) ^ {c}}$ ${\ displaystyle (n + c) ^ {c}}$ . Центральный вопрос сложности доказательства - понять, допускают ли тавтологии доказательства полиномиального размера. Формально

Задача (NP vs. coNP)

Существует ли полиномиально ограниченная пропозициональная система доказательств?

Кук и Рекхоу (1979) заметили, что существует полиномиально ограниченная система доказательств тогда и только тогда, когда NP = coNP. Следовательно, доказательство того, что конкретные системы доказательств не допускают доказательств полиномиального размера, можно рассматривать как частичный прогресс в направлении разделения NP и coNP (и, следовательно, P и NP).

Оптимальность и моделирование между системами доказательств

Сложность доказательства сравнивает силу систем доказательства с использованием понятия моделирования. Система доказательств P p-моделирует систему доказательств Q, если существует функция с полиномиальным временем, которая при заданном Q-доказательстве выдает P-доказательство той же тавтологии. Если P p-моделирует Q, а Q p-моделирует P, системы доказательств P и Q p-эквивалентны. Существует также более слабое понятие моделирования: система доказательств P моделирует систему доказательств Q, если существует многочлен p такой, что для каждого Q-доказательства x тавтологии A существует P-доказательство y точки A такое, что длина y, | y | не превосходит p (| x |).

Например, исчисление секвенций p-эквивалентно (каждой) системе Фреге.

Система доказательств p-оптимальна, если она p-моделирует все другие системы доказательств, и оптимальна, если он имитирует все другие системы доказательства. Вопрос о том, существуют ли такие системы доказательств, остается открытым:

Проблема (Оптимальность)

Существует ли p-оптимальная или оптимальная пропозициональная система доказательства?

Каждую пропозициональную систему доказательства P можно смоделировать с помощью Расширенного Фреге, расширенного с помощью аксиом, постулирующих разумность P. Известно, что существование оптимальной (соответственно p-оптимальной) системы доказательств следует из предположения, что NE = coNE (соответственно E = NE).

Известно, что для многих слабых систем доказательства они не моделируют некоторые более сильные системы (см. ниже). Однако вопрос остается открытым, если ослабить понятие моделирования. Например, остается открытым вопрос о том, эффективно ли Резолюция полиномиально моделирует Расширенный Фреге.

Автоматизируемость поиска доказательства

Важным вопросом сложности доказательства является понимание сложности поиска доказательств в системах доказательств.

Проблема (Автоматизируемость)

Существуют ли эффективные алгоритмы поиска доказательств в стандартных системах доказательств, таких как система Резолюции или Фреге?

Вопрос может быть формализован с помощью понятия автоматизируемости (также известной как автоматизируемость).

Система доказательств P автоматизируется, если существует алгоритм, который задан тавтологией $τ {\ displaystyle \ tau}$ $\ тау$ выводит P-доказательство $τ {\ displaystyle \ tau}$ $\ тау$ во временном полиноме размером $τ {\ displaystyle \ tau}$ $\ тау$ и длина самого короткого P-доказательства $τ {\ displaystyle \ tau}$ $\ тау$ . Обратите внимание, что если система доказательств не ограничена полиномиально, ее можно автоматизировать. Система доказательств P слабо автоматизируется, если существует система доказательств R и алгоритм, который с учетом тавтологии $τ {\ displaystyle \ tau}$ $\ тау$ выводит R-доказательство $τ {\ displaystyle \ tau}$ $\ тау$ по полиному времени размером $τ {\ displaystyle \ tau}$ $\ тау$ и длиной кратчайшего P-доказательства $τ {\ displaystyle \ tau}$ $\ тау$ .

Многие представляющие интерес системы доказательств считаются неавтоматическими. Однако в настоящее время известны лишь условно отрицательные результаты.

Krajíček и Pudlák (1998) доказали, что Extended Frege не является слабо автоматизируемым, если RSA не защищен от P / poly.
Bonet, Pitassi и Raz (2000) доказали, что $TC 0 {\ displaystyle TC ^ {0}}$ ${\ displaystyle TC ^ {0}}$ -Frege система не является слабо автоматизированной, если только схема Диффи-Хелмана не защищена от P / poly. Это было расширено Бонет, Доминго, Гавалда, Масиел и Питасси (2004), которые доказали, что системы Фреге с постоянной глубиной глубины не менее 2 не являются слабо автоматизируемыми, если только схема Диффи-Хелмана не защищена от неоднородных противников, работающих в субэкспоненциальном времени. 62>
Алехнович и Разборов (2008) доказали, что древовидные Разрешение и Разрешение не автоматизируются, если FPT = W [P]. Это было расширено Галези и Лаурией (2010), которые доказали, что Nullstellensatz и Полиномиальное исчисление нельзя автоматизировать, если иерархия фиксированных параметров не разрушается.
Mertz, Pitassi и Wei (2019) доказали, что древовидные Разрешение и Разрешение являются не автоматизируется при гипотезе экспоненциального времени.
Ацериас и Мюллер (2019) доказали, что разрешение нельзя автоматизировать, если P = NP. Де Резенде, Гёш, Нордстрём, Питасси, Робер и Соколов (2020) расширили это понятие до NP-сложности автоматизации Nullstellensatz, полиномиального исчисления, Шерали-Адамса; Гоэса, Корота, Мертца и Питасси (2020) на NP-твердость автоматизации плоскостей резки; и Гарлик (2020) к NP-сложности автоматизации разрешения k-DNF.

Неизвестно, нарушит ли слабая автоматизируемость разрешения любые стандартные предположения о сложности теории сложности.

С положительной стороны,

Бим и Питасси (1996) показали, что древовидное разрешение можно автоматизировать за квазиполиномиальное время, а разрешение можно автоматизировать по формулам малой ширины за слабо субэкспоненциальное время.

Ограниченная арифметика

Системы пропозициональных доказательств можно интерпретировать как неоднородные эквиваленты теорий более высокого порядка. Эквивалентность чаще всего изучается в контексте теорий ограниченной арифметики. Например, расширенная система Фреге соответствует теории Кука $PV 1 {\ displaystyle PV_ {1}}$ ${\ displaystyle PV_ {1}}$ формализации рассуждений за полиномиальное время, а система Фреге соответствует теории $VNC 1 {\ displaystyle VNC ^ {1}}$ ${\ displaystyle VNC ^ {1}}$ формализация $NC 1 {\ displaystyle NC ^ {1}}$ $NC ^ 1$ рассуждения.

Соответствие было введено Стивеном Куком (1975), который показал, что теоремы coNP формально $Π 1 b {\ displaystyle \ Pi _ {1} ^ {b}}$ ${\ displaystyle \ Pi _ {1} ^ {b}}$ формулы теории $PV 1 {\ displaystyle PV_ {1}}$ ${\ displaystyle PV_ {1}}$ преобразуются в последовательности тавтологий с доказательствами полиномиального размера в Расширенном Фреге. Более того, Расширенная Фреге является самой слабой такой системой: если другая система доказательств P обладает этим свойством, то P имитирует Расширенный Фреге.

Альтернативный перевод между утверждениями второго порядка и пропозициональными формулами, данный Джеффом Пэрис и Alex Wilkie (1985) был более практичным для захвата подсистем Расширенного Фреге, таких как Фреге или Фреге постоянной глубины.

Хотя вышеупомянутое соответствие говорит, что доказательства в теории Если перейти к последовательности коротких доказательств в соответствующей системе доказательств, то также имеет место обратная импликация. Можно получить нижние оценки размера доказательств в системе доказательств P, построив подходящие модели теории T, соответствующей системе P. Это позволяет доказать нижние оценки сложности с помощью теоретико-модельных построений, подхода, известного как метод Айтаи.

SAT-решатели

Системы пропозициональных доказательств можно интерпретировать как недетерминированные алгоритмы для распознавания тавтологий. Таким образом, доказательство суперполиномиальной нижней границы для системы доказательств P исключает существование полиномиального алгоритма для SAT, основанного на P. Например, прогоны алгоритма DPLL на неудовлетворительных экземплярах соответствуют древовидным опровержениям Резолюции. Следовательно, экспоненциальные нижние границы для древовидного разрешения (см. Ниже) исключают существование эффективных алгоритмов DPLL для SAT. Точно так же нижние границы экспоненциального разрешения подразумевают, что решатели SAT, основанные на разрешении, такие как алгоритмы CDCL, не могут эффективно решать SAT (в худшем случае).

Нижние оценки

Доказательство нижних оценок длины пропозициональных доказательств, как правило, очень сложно. Тем не менее было обнаружено несколько методов доказательства нижних оценок для слабых систем доказательства.

Хакен (1985) доказал экспоненциальную нижнюю границу для разрешения и принципа ячейки.
Аджтаи (1988) доказал суперполиномиальную нижнюю границу для системы Фреге постоянной глубины и принципа ячейки. Это было усилено до экспоненциальной нижней границы Крайичеком, Пудлаком и Вудсом, а также Питасси, Бимом и Импальяццо. Нижняя граница Айтая использует метод случайных ограничений, который также использовался для получения нижних границ AC в сложности схемы.
Крайичек (1994) сформулировал метод допустимой интерполяции, а затем использовал его для получения новых нижних границ. оценки для Резолюции и других систем доказательства.
Пудлак (1997) доказал экспоненциальные нижние границы для секущих плоскостей с помощью допустимой интерполяции.
Бен-Сассон и Вигдерсон (1999) предоставили метод доказательства, снижающий нижние границы от размера опровержений Резолюции до нижних границ ширины опровержений Резолюции, которые охватывают многие обобщения нижней границы Хакена.

Вывести нетривиальную нижнюю границу для системы Фреге - давняя открытая проблема.

Возможная интерполяция

Рассмотрим тавтологию вида $A (x, y) → B (y, z) {\ displaystyle A (x, y) \ rightarrow B (y, z)}$ $A (x, y) \ rightarrow B (y, z)$ . Тавтология верна для любого выбора $y {\ displaystyle y}$ $y$ , и после исправления $y {\ displaystyle y}$ $y$ оценка $A { \ displaystyle A}$ $A$ и $B {\ displaystyle B}$ $B$ независимы, потому что они определены на непересекающихся наборах переменных. Это означает, что можно определить схему интерполянта $C (y) {\ displaystyle C (y)}$ $C (y)$ , такую, что оба $A (x, y) → C (y) {\ Displaystyle A (x, y) \ rightarrow C (y)}$ $A (x, y) \ rightarrow C (y)$ и $C (y) → B (y, z) {\ displaystyle C (y) \ rightarrow B (y, z)}$ $C (y) \ rightarrow B (y, z)$ удерживать. Схема интерполянта решает, является ли $A (x, y) {\ displaystyle A (x, y)}$ $A (x, y)$ ложным или $B (y, z) {\ displaystyle B (y, z)}$ $B(y,z)$ верно только при учете $y {\ displaystyle y}$ $y$ . Характер схемы интерполянта может быть произвольным. Тем не менее, можно использовать доказательство исходной тавтологии $A (x, y) → B (y, z) {\ displaystyle A (x, y) \ rightarrow B (y, z)}$ $A (x, y) \ rightarrow B (y, z)$ как подсказка о том, как построить $C {\ displaystyle C}$ $C$ . Говорят, что система доказательств P имеет допустимую интерполяцию, если интерполянт $C (y) {\ displaystyle C (y)}$ $C (y)$ эффективно вычислим из любого доказательства тавтологии $A (x, y) → B (y, z) {\ displaystyle A (x, y) \ rightarrow B (y, z)}$ $A (x, y) \ rightarrow B (y, z)$ в P. Эффективность измеряется по длине доказательства: это легче вычислить интерполянты для более длинных доказательств, поэтому это свойство кажется антимонотонным по силе системы доказательств.

Следующие три утверждения не могут быть одновременно верными: (a) $A (x, y) → B (y, z) {\ displaystyle A (x, y) \ rightarrow B (y, z)}$ $A (x, y) \ rightarrow B (y, z)$ имеет короткое доказательство в некоторой системе доказательств; (б) такая система доказательств имеет допустимую интерполяцию; (c) схема интерполянта решает вычислительно трудную задачу. Ясно, что из (a) и (b) следует, что существует небольшая схема интерполяции, что противоречит (c). Такое соотношение позволяет превратить верхние границы длины доказательства в нижние оценки вычислений и, вдвойне, превратить эффективные алгоритмы интерполяции в нижние границы длины доказательства.

Некоторые системы проверки, такие как разрешающая способность и плоскости разреза, допускают допустимую интерполяцию или ее варианты.

Возможная интерполяция может рассматриваться как слабая форма автоматизируемости. В частности, многие системы доказательств P способны доказать свою собственную надежность, что является тавтологией, утверждающей, что ʻif $π {\ displaystyle \ pi}$ $\ pi$ является P-доказательством формулы $ϕ ( x) {\ displaystyle \ phi (x)}$ $\ phi (x)$ , затем $ϕ (x) {\ displaystyle \ phi (x)}$ $\ phi (x)$ держит ». Здесь $π, ϕ, x {\ displaystyle \ pi, \ phi, x}$ ${\ displaystyle \ pi, \ phi, x}$ кодируются свободными переменными. Следовательно, эффективный интерполянт, полученный в результате коротких P-доказательств правильности P, будет определять, допускает ли данная формула $ϕ {\ displaystyle \ phi}$ $\ phi$ короткое P-доказательство $π {\ displaystyle \ pi}$ $\ pi$ . Однако в принципе было бы сложно создать такой интерполянт, если бы нам предоставили только формулу $ϕ {\ displaystyle \ phi}$ $\ phi$ . Более того, если система доказательств P не доказывает эффективно свою собственную надежность, то она не может быть слабо автоматизируемой, даже если она допускает допустимую интерполяцию. С другой стороны, из слабой автоматизируемости системы доказательств P следует, что P допускает допустимую интерполяцию.

Многие результаты неавтоматизируемости фактически являются свидетельством против возможной интерполяции в соответствующих системах.

Krajíček и Pudlák (1998) доказали, что Extended Frege не допускает выполнимой интерполяции, если RSA не защищен от P / poly.
Bonet, Pitassi and Raz (2000) доказали, что $TC 0 { \ displaystyle TC ^ {0}}$ ${\ displaystyle TC ^ {0}}$ -Frege система не допускает допустимой интерполяции, если схема Диффи-Хелмана не защищена от P / poly.
Бонет, Доминго, Гавальда, Масиэль, Питасси (2004) доказал, что системы Фреге постоянной глубины не допускают допустимой интерполяции, если только схема Диффи-Хелмана не защищена от неоднородных противников, работающих в субэкспоненциальном времени.

Неклассическая логика

Идея сравнения размер доказательств может использоваться для любой автоматизированной процедуры обоснования, которая генерирует доказательство. Было проведено некоторое исследование объема доказательств для пропозициональных неклассических логик, в частности, интуиционистских, модальных и немонотонных логик.

Хрубеш (2007-2009) доказал экспоненциальные нижние границы размера доказательств в расширенной системе Фреге в некоторых модальных логиках и интуиционистской логике, используя версию монотонной допустимой интерполяции.

См. Также

Ссылки

Дополнительная литература

Бим, Пол; Pitassi, Toniann (1998), «Сложность пропозиционального доказательства: прошлое, настоящее и будущее», Бюллетень Европейской ассоциации теоретической информатики, 65 : 66–89, MR 1650939, ECCC TR98-067
Кук, Стивен ; Нгуен, Фуонг (2010), Логические основы сложности доказательства, перспективы в логике, Кембридж: Cambridge University Press, doi : 10.1017 / CBO9780511676277, ISBN 978-0-521-51729-4, MR 2589550 (черновик от 2008 г. )
Крайичек, Ян (1995), Ограниченная арифметика, логика высказываний и теория сложности, Cambridge University Press
Крайичек, Ян ( 2005), «Сложность доказательства» (PDF), в Лаптев, А. (ред.), Труды 4-го Европейского математического конгресса, Цюрих: Европейское математическое общество, стр. 221–231, MR 2185746
Крайичек, Ян, Сложность доказательства, Cambridge University Press, 2019.
Пудлак, Павел (1998), «Длина доказательств», в Buss, SR (ред.), Справочник по теории доказательств, Исследования по логике и основам математики, 137, Амстердам: Северная Голландия, стр. 547–637, doi : 10.1016 / S0049-237X (98) 80023-2, MR 1640332

Внешние ссылки