Hispanopedia Wiki
Articulo de referencia

Complejidad de la prueba

En lógica y ciencias de la computación teórica , y específicamente en teoría de la demostración y teoría de la complejidad computacional , la complejidad de la demostración es e...

Hispanopedia WikiContenido en espanolLectura gratuita

En lógica y ciencias de la computación teórica , y específicamente en teoría de la demostración y teoría de la complejidad computacional , la complejidad de la demostración es el campo que busca comprender y analizar los recursos computacionales necesarios para probar o refutar enunciados. La investigación en complejidad de la demostración se centra principalmente en demostrar límites inferiores y superiores de longitud de demostración en diversos sistemas de demostración proposicional . Por ejemplo, uno de los principales desafíos de la complejidad de la demostración es demostrar que el sistema de Frege , el cálculo proposicional usual , no admite demostraciones de tamaño polinomial para todas las tautologías. Aquí, el tamaño de la demostración es simplemente el número de símbolos que contiene, y se dice que una demostración es de tamaño polinomial si es polinomial en el tamaño de la tautología que demuestra.

El estudio sistemático de la complejidad de las pruebas comenzó con el trabajo de Stephen Cook y Robert Reckhow (1979), quienes proporcionaron la definición básica de un sistema de prueba proposicional desde la perspectiva de la complejidad computacional. Específicamente, Cook y Reckhow observaron que demostrar cotas inferiores del tamaño de las pruebas en sistemas de prueba proposicionales cada vez más fuertes puede considerarse un paso hacia la separación de NP de co-NP (y, por lo tanto, de P de NP), ya que la existencia de un sistema de prueba proposicional que admita pruebas de tamaño polinomial para todas las tautologías es equivalente a NP = co-NP.

La investigación contemporánea sobre la complejidad de las pruebas se nutre de ideas y métodos de diversas áreas de la complejidad computacional, los algoritmos y las matemáticas. Dado que muchos algoritmos y técnicas algorítmicas importantes pueden formularse como algoritmos de búsqueda de pruebas para ciertos sistemas de prueba, demostrar cotas inferiores para el tamaño de las pruebas en estos sistemas implica establecer cotas inferiores para el tiempo de ejecución de los algoritmos correspondientes. Esto conecta la complejidad de las pruebas con áreas más aplicadas, como la resolución de problemas SAT .

La lógica matemática también puede servir como marco para estudiar la extensión de las pruebas proposicionales. Las teorías de primer orden y, en particular, los fragmentos débiles de la aritmética de Peano , conocidos como aritmética acotada , funcionan como versiones uniformes de los sistemas de pruebas proposicionales y proporcionan información adicional para interpretar pruebas proposicionales cortas en términos de diversos niveles de razonamiento factible.

Conceptos principales

Convenciones

Por defecto, la teoría de la demostración discutió los sistemas de demostración para la lógica proposicional clásica , utilizando el lenguaje de la lógica proposicional con los conectores.∧,∨,¬,→{\displaystyle \land ,\lor ,\neg ,\to }y una cantidad contable de variables proposicionales{pagi:i∈2∗}{\displaystyle \{p_{i}:i\in 2^{*}\}}. Aquí,2∗{\displaystyle 2^{*}}es el conjunto de cadenas binarias finitas.

Un sistema de prueba se denota con letras mayúsculas:PAG,Q,R,…{\displaystyle P,Q,R,\dots }Una demostración se denota con letras minúsculasincógnita,y,z,…{\displaystyle x,y,z,\dots }.

Una fórmula se representa con letras griegas minúsculas:ϕ,ψ,σ,…{\displaystyle \phi ,\psi ,\sigma ,\dots }La longitud de una fórmulaϕ{\displaystyle \phi }es|ϕ|{\displaystyle |\phi |}. De manera similar, la longitud de una pruebaincógnita{\displaystyle x}es|incógnita|{\displaystyle |x|}.

TAUT es un lenguaje formal que consta de las fórmulas tautológicas de la lógica proposicional.

La notación Big-O y Big-Omega se utiliza del mismo modo que en la teoría de la complejidad computacional.

Sistemas de prueba

Un sistema de prueba es un algoritmo.PAG{\displaystyle P}que requiere dos entradas: una fórmulaϕ{\displaystyle \phi }y una supuesta pruebaincógnita{\displaystyle x}El sistema de prueba debe satisfacer:

  • PAG(ϕ,incógnita){\displaystyle P(\phi ,x)}corre a tiempopagoly(|ϕ|,|incógnita|){\displaystyle {\mathsf {poly}}(|\phi |,|x|)}.
  • ϕ∈TAUT{\displaystyle \phi \in {\mathsf {TAUT}}}si y solo si existe algunaincógnita{\displaystyle x}, de tal manera quePAG(ϕ,incógnita){\displaystyle P(\phi ,x)}acepta.

Ejemplos de sistemas de prueba proposicionales incluyen el cálculo de secuentes , la resolución , los planos de corte y los sistemas de Frege . Las teorías matemáticas fuertes, como ZFC, también inducen sistemas de prueba proposicionales: una prueba de una tautología.τ{\displaystyle \tau }en una interpretación proposicional de ZFC es una prueba ZFC de una declaración formalizada 'τ{\displaystyle \tau }es una tautología.

Un sistema de prueba puede considerarse como un algoritmo no determinista de tiempo polinomial para probar la no satisfacibilidad. Es decir, dada una fórmulaϕ{\displaystyle \phi },ϕ{\displaystyle \phi }es insatisfacible si y solo si existe algúnincógnita{\displaystyle x}, de tal manera quePAG(¬ϕ,incógnita){\displaystyle P(\neg \phi ,x)}acepta. Esto demuestra su estrecha relación con la clase co-NP .

Complejidad

La teoría de la demostración convencional no se preocupa por qué fórmulas puede o no probar un sistema de demostración determinado. La complejidad de la demostración no se centra en lo que se puede hacer, sino en la eficiencia con la que se puede hacer, es decir, la complejidad computacional del sistema de demostración. Para medir la eficiencia, es necesario definir qué se entiende por eficiencia en un sistema de demostración.

En la teoría de la complejidad ordinaria, la eficiencia se puede medir por la cantidad de pasos necesarios ( complejidad temporal ), la cantidad de espacio de trabajo necesario ( complejidad espacial ), el tamaño de un circuito booleano necesario para implementar una función booleana ( complejidad del circuito ), etc. En la teoría de la complejidad de las pruebas, también existen varias formas de medir la eficiencia.

La complejidad de tamaño de un sistema de prueba denota el tamaño mínimo de pruebas posibles en el sistema para una tautología dada. En detalle, un sistema de prueba tiene una complejidad de tamaño (límite superior).O(F(norte)){\displaystyle O(F(n))}si y solo si se da alguna tautologíaϕ{\displaystyle \phi }de longitudnorte{\displaystyle n}, hay una prueba deϕ{\displaystyle \phi }en este sistema de prueba que utiliza≲F(norte){\displaystyle \lesssim F(n)}pasos. Tiene una complejidad de tamaño (límite inferior).Ω(F(norte)){\displaystyle \Omega (F(n))}si y solo si se le da cualquier longitudnorte{\displaystyle n}Existe una tautología.ϕ{\displaystyle \phi }de longitudnorte{\displaystyle n}, de tal manera que cualquier prueba deϕ{\displaystyle \phi }en el sistema de prueba se necesitan≳F(norte){\displaystyle \gtrsim F(n)}pasos.

La complejidad espacial de un sistema de prueba indica el uso de memoria durante una prueba. Una forma común de medir el "uso de memoria" es la complejidad de cláusulas : el número máximo de cláusulas que pueden aparecer simultáneamente durante una prueba de resolución . Otras formas de medir la complejidad espacial incluyen:

  • El número de símbolos de una demostración.
  • El número de líneas de una demostración.
  • La complejidad máxima de las fórmulas que aparecen en una demostración. La complejidad de una fórmula puede deberse a su longitud, al número de variables, al número de cuantificadores, etc.
  • La profundidad de un árbol de demostración (en el caso de la deducción natural o el cálculo de secuentes).
  • La complejidad de memoria de una demostración. Podemos imaginar un sistema de demostración como un banco de memoria, de modo que en cualquier punto de la demostración, solo se pueden usar las fórmulas o axiomas que contiene. Una fórmula puede eliminarse del banco de memoria, pero si se necesita volver a usar, debe demostrarse nuevamente. Entonces, la complejidad de memoria de la demostración es el número mínimo de ubicaciones de memoria necesarias para completar la demostración.

La complejidad de búsqueda de un sistema de prueba denota la complejidad computacional de un probador, es decir, un algoritmo para encontrar una prueba de una tautología dentro de un sistema de prueba. Un sistema de prueba con un probador de tiempo polinomial es automatizable .

Complejidad del tamaño de la prueba

p-acotación

Un sistema de pruebaPAG{\displaystyle P}es acotado polinomialmente ( p-acotado ) si y solo si para cualquierϕ{\displaystyle \phi }, si existe algunaincógnita{\displaystyle x}de tal manera quePAG(ϕ,incógnita){\displaystyle P(\phi ,x)}Si es cierto, entonces existe algúnincógnita{\displaystyle x}de tal manera quePAG(ϕ,incógnita){\displaystyle P(\phi ,x)}es cierto y|incógnita|=pagoly(|ϕ|){\displaystyle |x|={\mathsf {poly}}(|\phi |)}En otras palabras, cualquier cosa que el sistema pueda demostrar, tiene una demostración polinomialmente corta.

Se cree que la mayoría de los sistemas de prueba no triviales no están acotados por p. Para comprender intuitivamente por qué sucede esto, consideremos los siguientes ejemplos.

Coloreado de gráficos

Dado un gráficoGRAMO=(V,mi){\displaystyle G=(V,E)}Si existe una 3- coloración , entonces esto se puede demostrar simplemente dando la coloración. Por lo tanto, la prueba de la 3-colorabilidad tiene longitud|V|{\displaystyle |V|}Se puede comprobar en tiempo polinomial. Por el contrario, si no existe una 3-coloración, entonces no hay una forma obvia de demostrarlo sucintamente. La forma ingenua de demostrarlo es enumerar explícitamente todos3|V|{\displaystyle 3^{|V|}}posibles 3-coloraciones, y demostrando que en cada caso hay dos vértices del mismo color que comparten una arista. Sin embargo, dicha demostración es exponencialmente grande en comparación con el tamaño de la entrada.

La construcción de Hajós es un sistema de prueba sólido y completo para la no 3-colorabilidad de grafos: un grafo no es 3-coloreable si y solo si posee una 4-construcción de Hajós. Sin embargo, dicha construcción puede requerir un número superpolinomial de pasos.

Polinomio

Dado un sistema de polinomiosF1(incógnita1,…,incógnitanorte),…,Fmetro(incógnita1,…,incógnitanorte){\displaystyle f_{1}(x_{1},\dots ,x_{n}),\dots ,f_{m}(x_{1},\dots ,x_{n})}en un campo finitoF{\displaystyle \mathbb {F} }Si existe una raíz, esto se puede demostrar simplemente dando los valores de las variables.incógnita1,…,incógnitanorte{\displaystyle x_{1},\dots ,x_{n}}El tamaño de la prueba es lineal con respecto al tamaño de la entrada. Se puede verificar en tiempo polinomial.

Sin embargo, si no hay raíz, entonces no hay una forma obvia de demostrarlo sucintamente. La forma ingenua de demostrarlo es enumerar explícitamente todos|F|norte{\displaystyle |\mathbb {F} |^{n}}valores posibles. Por el Nullstellensatz de Hilbert , existe un sistema de prueba sólido y completo para la no resolubilidad: Existen algunos polinomiosgramo1,…,gramometro{\displaystyle g_{1},\dots ,g_{m}}de tal manera que∑i=1metrogramoiFi=1{\displaystyle \sum _{i=1}^{m}g_{i}f_{i}=1}, si y solo si el sistema polinómico no es resoluble. Sin embargo, los polinomiosgramo1,…,gramometro{\displaystyle g_{1},\dots ,g_{m}}puede contener una cantidad superpolinómica de términos.

Tautología

Dada una fórmulaϕ{\displaystyle \phi }en lógica proposicional clásica con variables proposicionalespag1,…,pagnorte{\displaystyle p_{1},\dots ,p_{n}}Si no es una tautología, entonces esto se puede demostrar simplemente dando los valores de verdad para las variables proposicionales.pag1,…,pagnorte{\displaystyle p_{1},\dots ,p_{n}}, de tal manera queϕ{\displaystyle \phi }se evalúa como Falso. El tamaño de la prueba es lineal con respecto al tamaño de la entrada. Sin embargo, si es una tautología, entonces no hay una forma obvia de probarla sucintamente. La forma ingenua de probarla es enumerar explícitamente la tabla de verdad , que tiene2norte{\displaystyle 2^{n}}filas.

Hay muchos sistemas de prueba sólidos y completos para probar tautologías de la lógica proposicional clásica, pero no hay garantía de que algún sistema pueda probar todas las tautologías con tamaño de prueba.pagoly(|ϕ|){\displaystyle {\mathsf {poly}}(|\phi |)}.

Resultados principales

Problema sin resolver en informática
¿Existe un sistema de demostración p-acotado para las tautologías proposicionales clásicas?
Más problemas sin resolver en informática

Porqueϕ{\displaystyle \phi }no es una tautología si y solo si¬ϕ{\displaystyle \neg \phi }es satisfactorio,TAUT{\displaystyle {\mathsf {TAUT}}}es co-NP-completo. Por lo tanto, si existe un sistema de prueba paraTAUT{\displaystyle {\mathsf {TAUT}}}que es p-acotado, entonces NP = co-NP. Recíprocamente, si NP = co-NP, entoncesTAUT{\displaystyle {\mathsf {TAUT}}}, al ser co-NP, también sería NP, y por lo tanto existe un sistema de prueba p-acotado para probar tautologías. Esto fue demostrado por primera vez por Cook y Reckhow (1979). [ 1 ] Esto resulta en una formulación equivalente del problema NP = coNP :

¿Existe un sistema de demostración p-acotado para las tautologías proposicionales clásicas?

Fuerza del sistema de prueba

La complejidad de las pruebas compara la solidez de los sistemas de prueba utilizando el concepto de simulación eficiente . La eficiencia es el concepto clave aquí, ya que la teoría de la complejidad de las pruebas no solo estudia si algo puede probarse, sino también la eficiencia de la prueba.

Definiciones

Dados dos sistemas de pruebaPAG,Q{\displaystyle P,Q},PAG{\displaystyle P}simulaQ{\displaystyle Q}, escrito comoPAG≤Q{\displaystyle P\leq Q}, si y solo si existe un algoritmo que:

  • Se le proporciona como entrada una prueba Q de una tautología, y produce una prueba P de la misma tautología.
  • y el tamaño de la prueba P es polinómico en el tamaño de la prueba Q.

Decimos quePAG{\displaystyle P}p-simulaQ{\displaystyle Q}, escrito comoPAG≤pagQ{\displaystyle P\leq _{p}Q}si y solo si existe un algoritmo que:

  • Se le proporciona como entrada una prueba Q de una tautología, y produce una prueba P de la misma tautología.
  • y se ejecuta en tiempo polinomial polinomial en el tamaño de la prueba Q.

Dado que un algoritmo de tiempo polinomial solo puede producir una salida de tamaño polinomial, la p-simulación implica simulación. Lo contrario puede no ser cierto, es decir, dos sistemas de prueba.PAG,Q{\displaystyle P,Q}puede existir tal quePAG{\displaystyle P}simulaQ{\displaystyle Q}, peroPAG{\displaystyle P}no simula pQ{\displaystyle Q}.

Tanto las relaciones de simulación como las de p-simulación son reflexivas y transitivas , por lo tanto son preórdenes e inducen relaciones de equivalencia. SiPAG,Q{\displaystyle P,Q}Si se (p)simulan entre sí, entonces son (p)equivalentes . Un sistema de prueba es (p)óptimo si (p)simula a todos los demás sistemas de prueba.

Resultados

Cualquier conjunto no vacío en NP tiene un sistema de prueba óptimo. No se conoce ningún conjunto fuera de NP que tenga un sistema de prueba óptimo. Se sabe que ningún conjunto coNE-difícil, e incluso todos los conjuntos coNQP-difíciles, tienen sistemas de prueba óptimos. [ 2 ]

El cálculo de secuencias es p-equivalente a (todo) sistema de Frege. [ 3 ]

Todo sistema de prueba proposicional P puede ser simulado por Frege extendido con axiomas que postulan la solidez de P. [ 4 ]

Problema sin resolver en informática
¿Existe un sistema de prueba proposicional p-óptimo u óptimo?
Más problemas sin resolver en informática

Un sistema de demostración proposicional óptimo o p-óptimo sería ideal en cierto sentido, ya que produciría las demostraciones más cortas (salvo un factor polinómico) posibles para todas las tautologías. Desafortunadamente, esta cuestión sigue abierta.

Se sabe que: [ 5 ]

  • Si E = NE , entonces existe un sistema de prueba óptimo.
  • Si NE = co-NE, entonces existe un sistema de prueba óptimo.

Se ha demostrado que muchos sistemas de prueba débiles no pueden simular ciertos sistemas más fuertes (véase más adelante). Sin embargo, la cuestión permanece abierta si se relaja la noción de simulación. Por ejemplo, queda por determinar si Resolution simula eficazmente el método de Frege extendido de forma polinómica. [ 6 ]

Automatización

La complejidad de búsqueda de los sistemas de prueba plantea: [ 7 ]

Dado un sistema de demostración, ¿existe en este sistema un probador eficiente de tautologías?

Un sistema de pruebaPAG{\displaystyle P}es automatizable si existe un algoritmoT{\displaystyle T}, llamado el probador , de tal manera que:

  • Siτ{\displaystyle \tau }es una tautología, entoncesPAG(τ,T(τ)){\displaystyle P(\tau ,T(\tau ))}es cierto. Es decir, el algoritmo produce una prueba P deτ{\displaystyle \tau }. Tenga en cuenta que no hay ningún requisito sobre lo que el algoritmo debe hacer cuandoτ{\displaystyle \tau }no es una tautología.
  • T(τ){\displaystyle T(\tau )}es computable en tiempopagoly(|τ|,|incógnita|){\displaystyle {\mathsf {poly}}(|\tau |,|x|)}, dóndeincógnita{\displaystyle x}es la prueba P más corta deτ{\displaystyle \tau }.

El segundo requisito incorpora la condición de "la prueba P más corta deτ{\displaystyle \tau }", de modo que, incluso si P no está acotado polinómicamente, aún puede automatizarse. Es decir, puede haber tautologías tales que el sistema de prueba P se vea obligado a demostrar con pruebas que crecen de forma superpolinómica. Sin embargo, el demostrador hace lo mejor que puede en una situación difícil."

En términos más generales, un sistema de pruebasPAG{\displaystyle P}es débilmente automatizable si existe otro sistema de prueba.R{\displaystyle R}y un probadorT{\displaystyle T}, de tal manera que:

  • Siτ{\displaystyle \tau }es una tautología, entoncesR(τ,T(τ)){\displaystyle R(\tau ,T(\tau ))}es cierto. Es decir, el algoritmo produce una prueba R deτ{\displaystyle \tau }.
  • T(τ){\displaystyle T(\tau )}es computable en tiempopagoly(|τ|,|incógnita|){\displaystyle {\mathsf {poly}}(|\tau |,|x|)}, dóndeincógnita{\displaystyle x}es la prueba P más corta deτ{\displaystyle \tau }.

Resultados

Se cree que muchos sistemas de prueba de interés no son automatizables. Sin embargo, actualmente solo se conocen resultados negativos condicionales.

  • Krajíček y Pudlák (1998) demostraron que Frege extendido no es débilmente automatizable a menos que RSA no sea seguro contra P/poly . [ 8 ]
  • Bonet , Pitassi y Raz (2000) demostraron que laTdo0{\displaystyle TC^{0}}-El sistema de Frege no es débilmente automatizable a menos que el esquema de Diffie-Hellman no sea seguro contra P/poly. [ 9 ] Esto fue extendido por Bonet, Domingo, Gavaldá, Maciel y Pitassi (2004), quienes demostraron que los sistemas de Frege de profundidad constante de profundidad al menos 2 no son débilmente automatizables a menos que el esquema de Diffie-Hellman no sea seguro contra adversarios no uniformes que trabajan en tiempo subexponencial. [ 10 ]
  • Alekhnovich y Razborov (2008) demostraron que Resolution y Resolution, de tipo árbol, no son automatizables a menos que FPT=W[P] . [ 11 ] Esto fue extendido por Galesi y Lauria (2010), quienes demostraron que Nullstellensatz y Polynomial Calculus no son automatizables a menos que la jerarquía de parámetros fijos colapse. [ 12 ] Mertz, Pitassi y Wei (2019) demostraron que Resolution y Resolution, de tipo árbol, no son automatizables incluso en cierto tiempo cuasipolinomial asumiendo la hipótesis del tiempo exponencial . [ 13 ]
  • Atserias y Müller (2019) demostraron que la Resolución no es automatizable a menos que P=NP. [ 14 ] Esto fue extendido por de Rezende, Göös, Nordström, Pitassi, Robere y Sokolov (2020) a la NP-dureza de la automatización del Nullstellensatz y el Cálculo Polinomial; [ 15 ] por Göös, Koroth, Mertz y Pitassi (2020) a la NP-dureza de la automatización de los Planos de Corte; [ 16 ] y por Garlík (2020) a la NP-dureza de la automatización de la Resolución k - DNF . [ 17 ]

Se desconoce si la débil capacidad de automatización de Resolution rompería alguna de las suposiciones estándar de complejidad teórica.

En el lado positivo,

  • Beame y Pitassi (1996) demostraron que la resolución tipo árbol es automatizable en tiempo cuasi-polinomial y que la resolución es automatizable en fórmulas de ancho pequeño en tiempo débilmente subexponencial. [ 18 ] [ 19 ]

Aritmética acotada

Los sistemas de prueba proposicionales pueden interpretarse como equivalentes no uniformes de teorías de orden superior. La equivalencia se estudia con mayor frecuencia en el contexto de teorías de aritmética acotada . Por ejemplo, el sistema de Frege extendido corresponde a la teoría de Cook.PAGV1{\displaystyle \mathrm {PV} _{1}}La formalización del razonamiento en tiempo polinomial y el sistema de Frege se corresponde con la teoría.Vnortedo1{\displaystyle \mathrm {VNC} ^{1}}formalizaciónnortedo1{\displaystyle {\mathsf {NC}}^{1}}razonamiento.

La correspondencia fue introducida por Stephen Cook (1975), quien demostró que los teoremas coNP, formalmenteΠ1b{\displaystyle \Pi _{1}^{b}}fórmulas, de la teoríaPAGV1{\displaystyle \mathrm {PV} _{1}}se traducen en secuencias de tautologías con pruebas de tamaño polinomial en Frege extendido. Además, Frege extendido es el sistema más débil de este tipo: si otro sistema de prueba P tiene esta propiedad, entonces P simula Frege extendido. [ 20 ]

Una traducción alternativa entre enunciados de segundo orden y fórmulas proposicionales dada por Jeff Paris y Alex Wilkie (1985) ha resultado más práctica para capturar subsistemas de Frege extendido, como Frege o Frege de profundidad constante. [ 21 ] [ 22 ]

Si bien la correspondencia mencionada anteriormente indica que las demostraciones en una teoría se traducen en secuencias de demostraciones cortas en el sistema de demostración correspondiente, también se cumple una implicación opuesta. Es posible obtener cotas inferiores para el tamaño de las demostraciones en un sistema de demostración P mediante la construcción de modelos adecuados de una teoría T que corresponda al sistema P. Esto permite demostrar cotas inferiores de complejidad mediante construcciones basadas en modelos , un enfoque conocido como el método de Ajtai . [ 23 ]

solucionadores SAT

Los sistemas de prueba proposicionales pueden interpretarse como algoritmos no deterministas para el reconocimiento de tautologías. Demostrar una cota inferior superpolinómica en un sistema de prueba P descarta la existencia de un algoritmo de tiempo polinomial para SAT basado en P. Por ejemplo, las ejecuciones del algoritmo DPLL en instancias insatisfacibles corresponden a refutaciones de Resolución con estructura de árbol. Por lo tanto, las cotas inferiores exponenciales para Resolución con estructura de árbol (véase más adelante) descartan la existencia de algoritmos DPLL eficientes para SAT. De manera similar, las cotas inferiores exponenciales de Resolución implican que los solucionadores de SAT basados ​​en Resolución, como los algoritmos CDCL, no pueden resolver SAT de manera eficiente (en el peor de los casos).

límites inferiores

Demostrar cotas inferiores para la longitud de las demostraciones proposicionales suele ser muy difícil. Sin embargo, se han descubierto varios métodos para demostrar cotas inferiores para sistemas de demostración débiles.

  • Haken (1985) demostró una cota inferior exponencial para la Resolución y el principio del palomar . [ 24 ]
  • Ajtai (1988) demostró una cota inferior superpolinómica para el sistema de Frege de profundidad constante y el principio del palomar. [ 25 ] Esta fue reforzada a una cota inferior exponencial por Krajíček, Pudlák y Woods [ 26 ] y por Pitassi, Beame e Impagliazzo. [ 27 ] La cota inferior de Ajtai utiliza el método de restricciones aleatorias, que también se utilizó para derivar cotas inferiores AC 0 en complejidad de circuitos .
  • Krajíček (1994) [ 28 ] formuló un método de interpolación factible y posteriormente lo utilizó para derivar nuevas cotas inferiores para Resolution y otros sistemas de prueba. [ 29 ]
  • Pudlák (1997) demostró cotas inferiores exponenciales para planos de corte mediante interpolación factible. [ 30 ]
  • Ben-Sasson y Wigderson (1999) proporcionaron un método de prueba que reduce los límites inferiores del tamaño de las refutaciones de Resolución a límites inferiores del ancho de las refutaciones de Resolución, que capturaron muchas generalizaciones del límite inferior de Haken. [ 19 ]

Derivar una cota inferior no trivial para el sistema de Frege es un problema abierto de larga data.

Interpolación factible

Consideremos una tautología de la formaA(incógnita,y)→B(y,z){\displaystyle A(x,y)\rightarrow B(y,z)}La tautología es cierta para cada elección dey{\displaystyle y}y después de arreglarloy{\displaystyle y}la evaluación deA{\displaystyle A}yB{\displaystyle B}son independientes porque están definidas en conjuntos disjuntos de variables. Esto significa que es posible definir un circuito interpolante.do(y){\displaystyle C(y)}, de tal manera que ambosA(incógnita,y)→do(y){\displaystyle A(x,y)\rightarrow C(y)}ydo(y)→B(y,z){\displaystyle C(y)\rightarrow B(y,z)}mantener. El circuito interpolante decide siA(incógnita,y){\displaystyle A(x,y)}es falso o siB(y,z){\displaystyle B(y,z)}es cierto, considerando únicamentey{\displaystyle y}La naturaleza del circuito interpolante puede ser arbitraria. Sin embargo, es posible utilizar una demostración de la tautología inicial.A(incógnita,y)→B(y,z){\displaystyle A(x,y)\rightarrow B(y,z)}como una pista sobre cómo construirdo{\displaystyle C}Se dice que un sistema de prueba P tiene interpolación factible si el interpolantedo(y){\displaystyle C(y)}es computable eficientemente a partir de cualquier prueba de la tautología.A(incógnita,y)→B(y,z){\displaystyle A(x,y)\rightarrow B(y,z)}en P. La eficiencia se mide con respecto a la longitud de la prueba: es más fácil calcular interpolantes para pruebas más largas, por lo que esta propiedad parece ser antimonótona en la fuerza del sistema de prueba.

Las siguientes tres afirmaciones no pueden ser verdaderas simultáneamente: (a)A(incógnita,y)→B(y,z){\displaystyle A(x,y)\rightarrow B(y,z)}tiene una prueba corta en algún sistema de prueba; (b) dicho sistema de prueba tiene una interpolación factible; (c) el circuito interpolante resuelve un problema computacionalmente difícil. Es evidente que (a) y (b) implican que existe un circuito interpolante pequeño, lo cual contradice (c). Esta relación permite convertir los límites superiores de la longitud de la prueba en límites inferiores de los cálculos, y, de forma dual, convertir los algoritmos de interpolación eficientes en límites inferiores de la longitud de la prueba.

Algunos sistemas de prueba, como Resolución y Planos de Corte, admiten interpolación factible o sus variantes. [ 29 ] [ 30 ]

La interpolación factible puede considerarse una forma débil de automatización. De hecho, para muchos sistemas de prueba, como el de Frege extendido, la interpolación factible es equivalente a la automatización débil. Específicamente, muchos sistemas de prueba P son capaces de demostrar su propia solidez, lo cual es una tautología.RmiFPAG(π,ϕ,incógnita){\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}afirmando que `siπ{\displaystyle \pi }es una prueba P de una fórmulaϕ(incógnita){\displaystyle \phi (x)}entoncesϕ(incógnita){\displaystyle \phi (x)}sostiene'. Aquí,π,ϕ,incógnita{\displaystyle \pi ,\phi ,x}están codificadas por variables libres. Además, es posible generar pruebas P deRmiFPAG(π,ϕ,incógnita){\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}en tiempo polinomial dada la longitud deπ{\displaystyle \pi }yϕ{\displaystyle \phi }Por lo tanto, un interpolante eficiente resultante de breves pruebas P de solidez de P decidiría si una fórmula dadaϕ{\displaystyle \phi }admite una prueba P cortaπ{\displaystyle \pi }Dicho interpolante puede utilizarse para definir un sistema de prueba R que atestigua que P es débilmente automatizable. [ 31 ] Por otro lado, la débil automatización de un sistema de prueba P implica que P admite interpolación factible. Sin embargo, si un sistema de prueba P no prueba eficientemente su propia solidez, entonces podría no ser débilmente automatizable incluso si admite interpolación factible.

Muchos resultados que demuestran la falta de automatización evidencian que la interpolación no es factible en los sistemas respectivos.

  • Krajíček y Pudlák (1998) demostraron que Frege extendido no admite interpolación factible a menos que RSA no sea seguro contra P/poly. [ 32 ]
  • Bonet, Pitassi y Raz (2000) demostraron que laTdo0{\displaystyle TC^{0}}-El sistema Frege no admite interpolación factible a menos que el esquema Diffie-Helman no sea seguro contra P/poly. [ 33 ]
  • Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) demostraron que los sistemas de Frege de profundidad constante no admiten interpolación factible a menos que el esquema Diffie-Helman no sea seguro contra adversarios no uniformes que trabajan en tiempo subexponencial. [ 34 ]

Lógicas no clásicas

Muchas de estas preguntas también pueden plantearse sobre lógicas proposicionales no clásicas , como las lógicas intuicionistas , modales y no monótonas .

Hrubeš (2007–2009) demostró cotas inferiores exponenciales en el tamaño de las pruebas en el sistema de Frege extendido en algunas lógicas modales y en lógica intuicionista utilizando una versión de interpolación factible monótona. [ 35 ] [ 36 ] [ 37 ]

Véase también

Referencias

  1. ↑ Cook, Stephen ; Reckhow, Robert A. (1979). "La eficiencia relativa de los sistemas de prueba proposicionales". Journal of Symbolic Logic . 44 (1): 36– 50. doi : 10.2307/2273702 . JSTOR 2273702. S2CID 2187041 .  
  2. ↑ Dose, Titus; Glaßer, Christian (2019-04-02), NP-Completitud, Sistemas de Prueba y Pares NP Disjuntos , Coloquio Electrónico sobre Complejidad Computacional, TR19-050
  3. ↑ Reckhow, Robert A. (1976). Sobre la longitud de las demostraciones en el cálculo proposicional (Tesis doctoral). Universidad de Toronto.
  4. ↑ Krajíček, enero (2019). Complejidad de la prueba . Prensa de la Universidad de Cambridge.
  5. ↑ Krajíček, Jan; Pudlák, Pavel (1989). "Sistemas de prueba proposicionales, la consistencia de las teorías de primer orden y la complejidad de los cálculos". Journal of Symbolic Logic . 54 (3): 1063– 1079. doi : 10.2307/2274765 . JSTOR 2274765 . S2CID 15093234 .  
  6. ↑ Pitassi, Toniann ; Santhanam, Rahul (2010). "Simulaciones efectivamente polinomiales" (PDF) . ICS : 370–382 .
  7. ↑ Bonet, ML ; Pitassi, Toniann ; Raz, Ran (2000). "Sobre la interpolación y automatización para el sistema de prueba de Frege". SIAM Journal on Computing . 29 (6): 1939– 1967. doi : 10.1137/S0097539798353230 .
  8. ↑ Krajíček, enero; Pudlák, Pavel (1998). "Algunas consecuencias de las conjeturas criptográficas paraS21{\displaystyle S_{2}^{1}}y EF" . Información y Computación . 140 (1): 82–94 . doi : 10.1006/inco.1997.2674 .
  9. ↑ Bonet, ML ; Pitassi, Toniann ; Raz, Ran (2000). "Sobre la interpolación y automatización para el sistema de prueba de Frege". SIAM Journal on Computing . 29 (6): 1939– 1967. doi : 10.1137/S0097539798353230 .
  10. ↑ Bonet, ML ; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "No automatizabilidad de las pruebas de Frege de profundidad limitada". Computational Complexity . 13 ( 1–2 ): 47–68 . doi : 10.1007/s00037-004-0183-5 . S2CID 1360759 . 
  11. ↑ Alekhnovich, Michael; Razborov, Alexander (2018). "La resolución no es automatizable a menos que W[P] sea tratable". SIAM Journal on Computing . 38 (4): 1347– 1363. doi : 10.1137/06066850X .
  12. ↑ Galesi, Nicola; Lauria, Massimo (2010). "Sobre la automatizabilidad del cálculo polinomial". Theory of Computing Systems . 47 (2): 491– 506. doi : 10.1007/s00224-009-9195-5 . S2CID 11602606 . 
  13. ↑ Mertz, Ian; Pitassi, Toniann; Wei, Yuanhao (2019). "Las demostraciones cortas son difíciles de encontrar". ICALP .
  14. ↑ Atserias, Albert ; Müller, Moritz (2019). "Automatizar la resolución es NP-difícil". Actas del 60.º Simposio sobre Fundamentos de la Informática . págs. 498–509 . 
  15. ^ de Rezende, Susana; Göös, Mika; Nordström, Jakob; Pitassi, Tonniano; Robere, Robert; Sokolov, Dmitry (2020). "La automatización de sistemas de prueba algebraica es NP-difícil". ECCC .
  16. ↑ Göös, Mika; Koroth, Sajín; Mertz, Ian; Pitassi, Tonniano (2020). "La automatización de planos de corte es NP-difícil". Actas del 52º Simposio Anual ACM SIGACT sobre Teoría de la Computación . págs. 68– 77. arXiv : 2004.08037 . doi : 10.1145/3357713.3384248 . ISBN  9781450369794. S2CID 215814356 . 
  17. ↑ Garlík, Michal (2020). "Fallo de la propiedad de disyunción factible para la resolución k -DNF y la NP-dificultad de automatizarla". ECCC . arXiv : 2003.10230 .
  18. ↑ Beame, Paul ; Pitassi, Toniann (1996). "Límites inferiores de resolución simplificados y mejorados". 37º Simposio Anual sobre Fundamentos de la Informática : 274–282 .
  19. 1 2 Ben-Sasson, Eli ; Wigderson, Avi (1999). "Las pruebas cortas son estrechas: la resolución se simplifica". Actas del 31.er Simposio ACM sobre Teoría de la Computación . págs. 517–526 . 
  20. ↑ Cook, Stephen (1975). "Pruebas constructivas factibles y el cálculo proposicional". Actas del 7.º Simposio Anual de la ACM sobre Teoría de la Computación . págs. 83–97 . 
  21. ↑ Paris, Jeff ; Wilkie, Alex (1985). «Problemas de conteo en aritmética acotada». Métodos en lógica matemática . Notas de clase en matemáticas. Vol. 1130. págs. 317–340 . doi : 10.1007/BFb0075316 . ISBN   978-3-540-15236-1.
  22. ↑ Cook, Stephen ; Nguyen, Phuong (2010). Fundamentos lógicos de la complejidad de las pruebas . Perspectivas en lógica. Cambridge: Cambridge University Press. doi : 10.1017/CBO9780511676277 . ISBN 978-0-521-51729-4MR 2589550 .​ ( borrador de 2008 )
  23. ↑ Ajtai, M. (1988). "La complejidad del principio del palomar". Actas del 29º Simposio Anual del IEEE sobre Fundamentos de la Informática . págs. 346–355 . 
  24. ↑ Haken, A. (1985). "La intratabilidad de la resolución". Theoretical Computer Science . 39 : 297–308 . doi : 10.1016/0304-3975(85)90144-6 .
  25. ↑ Ajtai, M. (1988). "La complejidad del principio del palomar". Actas del 29º Simposio Anual del IEEE sobre Fundamentos de la Informática . págs. 346–355 . 
  26. ↑ Krajíček, Jan; Pudlák, Pavel ; Woods, Alan (1995). "Una cota inferior exponencial para el tamaño de las pruebas de Frege de profundidad acotada del principio del palomar". Random Structures and Algorithms . 7 (1): 15– 39. doi : 10.1002/rsa.3240070103 .
  27. ↑ Pitassi, Toniann ; Beame, Paul ; Impagliazzo, Russell (1993). "Límites inferiores exponenciales para el principio del palomar". Computational Complexity . 3 (2): 97–308 . doi : 10.1007/BF01200117 . S2CID 1046674 . 
  28. ↑ Krajíček, Jan (1994). "Límites inferiores al tamaño de las pruebas proposicionales de profundidad constante". Journal of Symbolic Logic . 59 (1): 73– 86. doi : 10.2307/2275250 . JSTOR 2275250. S2CID 44670202 .  
  29. 1 2 Krajíček, Jan (1997). "Teoremas de interpolación, cotas inferiores para sistemas de prueba y resultados de independencia para aritmética acotada". Journal of Symbolic Logic . 62 (2): 69– 83. doi : 10.2307/2275541 . JSTOR 2275541 . S2CID 28517300 .  
  30. 1 2 Pudlák, Pavel (1997). "Límites inferiores para la resolución y las demostraciones de planos de corte y los cálculos monótonos". Journal of Symbolic Logic . 62 (3): 981– 998. doi : 10.2307/2275583 . JSTOR 2275583 . S2CID 8450089 .  
  31. ↑ Pudlák, Pavel (2003). " Sobre la reducibilidad y la simetría de pares NP disjuntos". Theoretical Computer Science . 295 : 323–339 . doi : 10.2307/2275583 . JSTOR 2275583. S2CID 8450089 .  
  32. ↑ Krajíček, enero; Pudlák, Pavel (1998). "Algunas consecuencias de las conjeturas criptográficas paraS21{\displaystyle S_{2}^{1}}y EF" . Información y Computación . 140 (1): 82–94 . doi : 10.1006/inco.1997.2674 .
  33. ↑ Bonet, ML ; Pitassi, Toniann ; Raz, Ran (2000). "Sobre la interpolación y automatización para el sistema de prueba de Frege". SIAM Journal on Computing . 29 (6): 1939– 1967. doi : 10.1137/S0097539798353230 .
  34. ↑ Bonet, ML ; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "No automatizabilidad de las pruebas de Frege de profundidad limitada". Computational Complexity . 13 ( 1–2 ): 47–68 . doi : 10.1007/s00037-004-0183-5 . S2CID 1360759 . 
  35. ↑ Hrubeš, Pavel (2007). "Límites inferiores para lógicas modales". Journal of Symbolic Logic . 72 (3): 941– 958. doi : 10.2178/jsl/1191333849 . S2CID 1743011 . 
  36. ↑ Hrubeš, Pavel (2007). "Un límite inferior para la lógica intuicionista". Anales de lógica pura y aplicada . 146 (1): 72– 90. doi : 10.1016/j.apal.2007.01.001 .
  37. ↑ Hrubeš, Pavel (2009). "Sobre la longitud de las demostraciones en lógicas no clásicas" . Anales de lógica pura y aplicada . 157 ( 2–3 ): 194–205 . doi : 10.1016/j.apal.2008.09.013 .

Lecturas adicionales

  • Beame, Paul; Pitassi, Toniann (1998), "Complejidad de la prueba proposicional: pasado, presente y futuro", Boletín de la Asociación Europea de Ciencias de la Computación Teórica , 65 : 66–89 , MR 1650939 , ECCC TR98-067  
  • Cook, Stephen ; Nguyen, Phuong (2010), Fundamentos lógicos de la complejidad de las pruebas , Perspectivas en lógica, Cambridge: Cambridge University Press, doi : 10.1017/CBO9780511676277 , ISBN 978-0-521-51729-4, MR 2589550 ( borrador de 2008 )
  • Pudlák, Pavel (1998), "La longitud de las demostraciones", en Buss, SR (ed.), Manual de teoría de la demostración , Estudios en lógica y fundamentos de las matemáticas, vol.  137, Ámsterdam: North-Holland, pp. 547–637 , doi : 10.1016/S0049-237X(98)80023-2 , ISBN  978-0-444-89840-1, MR 1640332 
  • Krajíček, Jan (1995). Aritmética acotada, lógica proposicional y teoría de la complejidad . Enciclopedia de matemáticas y sus aplicaciones. Cambridge [Inglaterra]  ; Nueva York, NY, EE. UU.: Cambridge University Press. ISBN 978-0-521-45205-2.
  • Krajíček, Jan (2005), "Complejidad de la demostración" (PDF) , en Laptev, A. (ed.), Actas del 4.º Congreso Europeo de Matemáticas , Zúrich: Sociedad Matemática Europea, pp. 221–231 , MR 2185746  
  • Krajíček, Jan (2019). Complejidad de la demostración . Enciclopedia de las matemáticas y sus aplicaciones. Cambridge: Cambridge University Press. ISBN 978-1-108-41684-9.
  • Complejidad de la prueba
  • Lista de correo sobre complejidad de las pruebas.