En la lógica y la informática teórica , y específicamente en la teoría de la prueba y la teoría de la complejidad computacional , la complejidad de la prueba es el campo que tiene como objetivo comprender y analizar los recursos computacionales que se requieren para probar o refutar declaraciones. La investigación en la complejidad de la prueba se ocupa principalmente de probar los límites superior e inferior de la longitud de la prueba en varios sistemas de prueba proposicionales . Por ejemplo, uno de los principales desafíos de la complejidad de la prueba es mostrar que el sistema de Frege , el cálculo proposicional habitual, no admite pruebas de tamaño polinómico de todas las tautologías; aquí el tamaño de la prueba es simplemente el número de símbolos que contiene, y se dice que una prueba es de tamaño polinomial si es polinomial en el tamaño de la tautología que prueba.
El estudio sistemático de la complejidad de la prueba 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 probar los límites inferiores del tamaño de la prueba en sistemas de prueba proposicionales cada vez más fuertes puede verse como un paso hacia la separación de NP de coNP (y por lo tanto P de NP), ya que la existencia de un sistema de prueba proposicional que admite pruebas de tamaño polinómico para todas las tautologías es equivalente a NP = coNP.
La investigación contemporánea de la complejidad de las pruebas extrae ideas y métodos de muchas áreas de la complejidad computacional, los algoritmos y las matemáticas. Dado que muchos algoritmos y técnicas algorítmicas importantes se pueden convertir como algoritmos de búsqueda de pruebas para ciertos sistemas de pruebas, demostrar límites inferiores en los tamaños de prueba en estos sistemas implica límites inferiores en el tiempo de ejecución de los algoritmos correspondientes. Esto conecta la complejidad de la prueba con áreas más aplicadas, como la resolución de SAT .
La lógica matemática también puede servir como marco para estudiar los tamaños de prueba proposicionales. Las teorías de primer orden y, en particular, los fragmentos débiles de la aritmética de Peano , que se denominan teorías aritméticas limitadas , sirven como versiones uniformes de los sistemas de prueba proposicionales y proporcionan más antecedentes para interpretar pruebas proposicionales breves en términos de varios niveles de razonamiento factible.
Sistemas de prueba
Un sistema de prueba proposicional se da como un algoritmo de verificación de prueba P ( A , x ) con dos entradas. Si P acepta el par ( A , x ) se dice que x es un P -proof de A . Se requiere que P se ejecute en tiempo polinomial y, además, debe sostener que A tiene una prueba P si y solo si es una tautología.
Ejemplos de sistemas de prueba proposicionales incluyen cálculo secuencial , resolución , planos de corte y sistema de Frege . Las teorías matemáticas sólidas como ZFC también inducen sistemas de prueba proposicionales: una prueba de una tautología en una interpretación proposicional de ZFC es una prueba de ZFC de una declaración formalizada ' es una tautología '.
Pruebas del tamaño del polinomio y el problema NP versus coNP
La complejidad de la prueba mide la eficiencia del sistema de prueba generalmente en términos del tamaño mínimo de pruebas posibles en el sistema para una tautología determinada. El tamaño de una prueba (fórmula resp.) Es el número de símbolos necesarios para representar la prueba (fórmula resp.). Un sistema de prueba proposicional P está acotado polinomialmente si existe una constante tal que toda tautología de tamaño tiene una prueba P de tamaño. Una cuestión central de la complejidad de las pruebas es comprender si las tautologías admiten pruebas de tamaño polinomial. Formalmente,
Problema (NP frente a coNP)
¿Existe un sistema de prueba proposicional acotado polinomialmente?
Cook y Reckhow (1979) observaron que existe un sistema de prueba acotado polinomialmente si y solo si NP = coNP. Por lo tanto, probar que los sistemas de prueba específicos no admiten pruebas de tamaño polinómico puede verse como un progreso parcial hacia la separación de NP y coNP (y por lo tanto P y NP). [1]
Optimidad y simulaciones entre sistemas de prueba
La complejidad de la prueba compara la fuerza de los sistemas de prueba utilizando la noción de simulación. Un sistema de prueba P p-simula un sistema de prueba Q si hay una función de tiempo polinómico que le da un Q -proof salidas una P -proof de la misma tautología. Si P p-simula Q y Q p-simula P , los sistemas de prueba P y Q son p-equivalentes . También hay una noción más débil de la simulación: un sistema de prueba P simula un sistema de prueba Q si hay un polinomio p tal que para cada Q -proof x de una tautología A , hay un P -proof y de A tal que la longitud de y , | y | es como máximo p (| x |).
Por ejemplo, el cálculo secuencial es p-equivalente a (cada) sistema de Frege. [2]
Un sistema de prueba es p-óptimo si p- simula todos los demás sistemas de prueba, y es óptimo si simula todos los demás sistemas de prueba. Es un problema abierto si existen tales sistemas de prueba:
Problema (Optimidad)
¿Existe un sistema de prueba proposicional p-óptimo u óptimo?
Cada sistema de prueba proposicional P puede ser simulado por Extended Frege ampliar con axiomas postulando solidez de P . [3] Se sabe que la existencia de un sistema de prueba óptimo (resp. P-óptimo) se deriva del supuesto de que NE = coNE (resp. E = NE). [4]
Para muchos sistemas de prueba débil, se sabe que no simulan ciertos sistemas más fuertes (ver más abajo). Sin embargo, la cuestión permanece abierta si se relaja la noción de simulación. Por ejemplo, está abierto si Resolution simula polinomialmente de forma efectiva la frecuencia extendida. [5]
Automatización de la búsqueda de pruebas
Una cuestión importante en la complejidad de las pruebas es comprender la complejidad de la búsqueda de pruebas en los sistemas de pruebas.
Problema (capacidad de automatización)
¿Existen algoritmos eficientes que busquen pruebas en sistemas de prueba estándar como el sistema Resolution o Frege?
La pregunta puede formalizarse mediante la noción de automatizabilidad (también conocida como automatizabilidad). [6]
Un sistema de prueba P es automatizable si hay un algoritmo que, dada una tautologíaproduce una prueba P de en polinomio de tiempo en el tamaño de y la longitud de la prueba P más corta de. Tenga en cuenta que si un sistema de prueba no está acotado polinomialmente, aún puede ser automatizable. Un sistema de prueba P es débilmente automatizable si hay un sistema de prueba R y un algoritmo que da una tautologíaemite una prueba R de en polinomio de tiempo en el tamaño de y la longitud de la prueba P más corta de.
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 Extended Frege no es débilmente automatizable a menos que RSA no sea seguro contra P / poly . [7]
- Bonet, Pitassi y Raz (2000) demostraron que -El sistema Frege no es débilmente automatizable a menos que el esquema Diffie-Helman no sea seguro contra P / poly. [6] Esto fue extendido por Bonet, Domingo, Gavaldá, Maciel y Pitassi (2004) quienes demostraron que los sistemas Frege de profundidad constante de profundidad al menos 2 no son débilmente automatizables a menos que el esquema Diffie-Helman no sea seguro contra adversarios no uniformes que trabajen en niveles subexponenciales. hora. [8]
- Alekhnovich y Razborov (2008) demostraron que la resolución en forma de árbol y la resolución no son automatizables a menos que FPT = W [P]. [9] Esto fue ampliado 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. [10] Mertz, Pitassi y Wei (2019) demostraron que la Resolución y la Resolución en forma de árbol no son automatizables incluso en cierto tiempo cuasi-polinómico asumiendo la hipótesis del tiempo exponencial. [11]
- Atserias y Müller (2019) demostraron que la resolución no es automatizable a menos que P = NP. [12] Esto fue ampliado por de Rezende, Göös, Nordström, Pitassi, Robere y Sokolov (2020) a la dureza NP de la automatización de Nullstellensatz, Polynomial Calculus, Sherali-Adams; [13] de Göös, Koroth, Mertz y Pitassi (2020) sobre la dureza NP de los planos de corte automatizados; [14] y por Garlík (2020) a NP-dureza de automatizar la resolución k -DNF. [15]
No se sabe si la capacidad de automatización débil de la resolución rompería cualquier supuesto estándar de dureza de la teoría de la complejidad.
En el lado positivo,
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 las teorías de la aritmética acotada . Por ejemplo, el sistema Extended Frege corresponde a la teoría de Cook formalizar el razonamiento polinomial-temporal y el sistema de Frege corresponde a la teoría formalizando razonamiento.
La correspondencia ha sido introducida por Stephen Cook (1975), quien demostró que los teoremas de coNP, formalmente fórmulas, de la teoría traducir a secuencias de tautologías con pruebas de tamaño polinomial en Extended Frege. Además, Extended Frege es el sistema más débil: si otro sistema de prueba P tiene esta propiedad, entonces P simula Extended Frege. [18]
Una traducción alternativa entre enunciados de segundo orden y fórmulas proposicionales dada por Jeff Paris y Alex Wilkie (1985) ha sido más práctica para capturar subsistemas de Frege extendido como Frege o Frege de profundidad constante. [19] [20]
Si bien la correspondencia mencionada anteriormente dice que las pruebas en una teoría se traducen en secuencias de pruebas cortas en el sistema de prueba correspondiente, también se cumple una forma de la implicación opuesta. Es posible derivar límites inferiores en el tamaño de las pruebas en un sistema de prueba P mediante la construcción de modelos adecuados de una teoría T correspondiente al sistema P . Esto permite probar los límites inferiores de complejidad a través de construcciones teóricas de modelos, un enfoque conocido como método de Ajtai. [21]
Solucionadores de SAT
Los sistemas de prueba proposicional pueden interpretarse como algoritmos no deterministas para reconocer tautologías. Probar una superpolynomial límite inferior en un sistema de prueba P por lo tanto excluye la existencia de un algoritmo de tiempo polinómico para SAT basado en P . Por ejemplo, las ejecuciones del algoritmo DPLL en instancias insatisfactorias corresponden a refutaciones de resolución en forma de árbol. Por lo tanto, los límites inferiores exponenciales para la resolución en forma de árbol (ver más abajo) descartan la existencia de algoritmos DPLL eficientes para SAT. De manera similar, los límites inferiores de Resolución exponencial implican que los solucionadores 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 límites inferiores en las longitudes de las demostraciones proposicionales es generalmente muy difícil. Sin embargo, se han descubierto varios métodos para probar límites inferiores para sistemas de prueba débiles.
- Haken (1985) demostró un límite inferior exponencial para la resolución y el principio de casillero. [22]
- Ajtai (1988) demostró un límite inferior superpolinomial para el sistema de Frege de profundidad constante y el principio de casillero. [21] Esto fue reforzado a un límite inferior exponencial por Krajíček, Pudlák y Woods [23] y por Pitassi, Beame e Impagliazzo. [24] El límite inferior de Ajtai utiliza el método de restricciones aleatorias que también se utilizó para derivar los límites inferiores de AC 0 en la complejidad del circuito .
- Krajíček (1994) [25] formuló un método de interpolación factible y luego lo utilizó para derivar nuevos límites inferiores para la resolución y otros sistemas de prueba. [26]
- Pudlák (1997) demostró límites inferiores exponenciales para planos de corte mediante interpolación factible. [27]
- Ben-Sasson y Wigderson (1999) proporcionaron un método de prueba que reducía los límites inferiores en el tamaño de las refutaciones de Resolución a límites inferiores en el ancho de las refutaciones de Resolución, que capturaron muchas generalizaciones del límite inferior de Haken. [17]
Es un problema abierto de larga data derivar un límite inferior no trivial para el sistema de Frege.
Interpolación factible
Considere una tautología de la forma. . La tautología es cierta para cada elección de, y después de arreglar la evaluación de y son independientes porque se definen en conjuntos disjuntos de variables. Esto significa que es posible definir un circuito interpolante, tal que ambos y mantener. El circuito interpolante decide si es falso o si es cierto, solo considerando . La naturaleza del circuito interpolante puede ser arbitraria. Sin embargo, es posible utilizar una prueba de la tautología inicial. como una pista sobre cómo construir . Se dice que un sistema de prueba P tiene una interpolación factible si el interpolante es eficientemente computable a partir de cualquier prueba de tautología 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 anti-monótona en la fuerza del sistema de prueba.
Las siguientes tres afirmaciones no pueden ser simultáneamente verdaderas: (a) 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. Está claro que (a) y (b) implican que hay un pequeño circuito interpolante, que está en contradicción con (c). Tal relación permite convertir los límites superiores de la longitud de la prueba en límites inferiores en los cálculos, y doblemente convertir los algoritmos de interpolación eficientes en límites inferiores en la longitud de la prueba.
Algunos sistemas de prueba como Resolution y Cutting Planes admiten una interpolación factible o sus variantes. [26] [27]
La interpolación factible puede verse como una forma débil de automatizabilidad. De hecho, para muchos sistemas de prueba, como Extended Frege, la interpolación factible es equivalente a una capacidad de automatización débil. Específicamente, muchos sistemas de prueba P pueden probar su propia solidez, lo cual es una tautología. diciendo que si es una prueba P de una fórmula luego sostiene '. Aquí,están codificados por variables libres. Además, es posible generar pruebas P de en tiempo polinomial dada la longitud de y . Por lo tanto, un interpolante eficiente resultante de breves P -pruebas de solidez de P decidiría si una fórmula dadaadmite un corto P- prueba. Tal interpolador puede usarse para definir un sistema de prueba R que atestigüe que P es débilmente automatizable. [28] Por otro lado, la capacidad de automatización débil de un sistema de prueba P implica que P admite una interpolación factible. Sin embargo, si un sistema de prueba P no demuestra eficientemente su propia solidez, entonces podría no ser débilmente automatizable incluso si admite una interpolación factible.
Muchos resultados de no automatizabilidad proporcionan realmente una evidencia contra la interpolación factible en los sistemas respectivos.
- Krajíček y Pudlák (1998) demostraron que Extended Frege no admite una interpolación factible a menos que RSA no sea seguro contra P / poly. [7]
- Bonet, Pitassi y Raz (2000) demostraron que -El sistema Frege no admite una interpolación factible a menos que el esquema Diffie-Helman no sea seguro contra P / poly. [6]
- 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 trabajen en tiempo subexponencial. [8]
Lógicas no clásicas
La idea de comparar el tamaño de las pruebas se puede utilizar para cualquier procedimiento de razonamiento automatizado que genere una prueba. Se han realizado algunas investigaciones sobre el tamaño de las pruebas para las lógicas proposicionales no clásicas, en particular, las lógicas intuicionistas, modales y no monótonas.
Hrubeš (2007-2009) demostró límites inferiores exponenciales en el tamaño de las pruebas en el sistema Extended Frege en algunas lógicas modales y lógica intuicionista utilizando una versión de interpolación factible monótona. [29] [30] [31]
Ver también
- Complejidad computacional
- Complejidad del circuito
- Complejidad de la comunicación
- Lógica matemática
- Teoría de la prueba
- Clases de complejidad
- NP (complejidad)
- coNP
Referencias
- ^ Cook, Stephen ; Reckhow, Robert A. (1979). "La eficiencia relativa de los sistemas de prueba proposicionales". Revista de lógica simbólica . 44 (1): 36–50. doi : 10.2307 / 2273702 . JSTOR 2273702 .
- ^ Reckhow, Robert A. (1976). Sobre la extensión de las pruebas en el cálculo proposicional (Tesis Doctoral). Universidad de Toronto.
- ^ Krajíček, enero (2019). "Prueba de complejidad". Prensa de la Universidad de Cambridge .
- ^ Krajíček, Jan ; Pudlák, Pavel (1989). "Sistemas de prueba proposicional, la consistencia de las teorías de primer orden y la complejidad de los cálculos". Revista de lógica simbólica . 54 (3): 1063–1079. doi : 10.2307 / 2274765 . JSTOR 2274765 .
- ^ Pitassi, Toniann ; Santhanam, Rahul (2010). "Efectivamente simulaciones polinomiales" (PDF) . ICS : 370–382.
- ^ a b c Bonet, ML ; Pitassi, Toniann ; Raz, Ran (2000). "Sobre interpolación y automatización para Frege Proof System". Revista SIAM de Computación . 29 (6): 1939–1967. doi : 10.1137 / S0097539798353230 .
- ^ a b Krajíček, Jan ; Pudlák, Pavel (1998). "Algunas consecuencias de las conjeturas criptográficas paraand EF ". Information and Computation . 140 (1): 82-94. doi : 10.1006 / inco.1997.2674 .
- ^ a b Bonet, ML ; Domingo, C .; Gavaldá, R .; Maciel, A .; Pitassi, Toniann (2004). "No automatizabilidad de Frege Proofs de profundidad acotada". Complejidad computacional . 13 (1–2): 47–68. doi : 10.1007 / s00037-004-0183-5 . S2CID 1360759 .
- ^ Alekhnovich, Michael; Razborov, Alexander (2018). "La resolución no se puede automatizar a menos que W [P] sea manejable". Revista SIAM de Computación . 38 (4): 1347-1363. doi : 10.1137 / 06066850X .
- ^ Galesi, Nicola; Lauria, Massimo (2010). "Sobre la automatizabilidad del cálculo de polinomios". Teoría de los sistemas informáticos . 47 (2): 491–506. doi : 10.1007 / s00224-009-9195-5 . S2CID 11602606 .
- ^ Mertz, Ian; Pitassi, Toniann; Wei, Yuanhao (2019). "Las pruebas breves son difíciles de encontrar". ICALP .
- ^ 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.
- ^ de Rezende, Susanna; Göös, Mika; Nordström, Jakob; Pitassi, Tonnian; Robere, Robert; Sokolov, Dmitry (2020). "La automatización de sistemas de prueba algebraica es NP-hard". CCC .
- ^ Göös, Mika; Koroth, Sajin; Mertz, Ian; Pitassi, Tonnian (2020). "Automatizar planos de corte es NP-hard". STOC : 68–77. arXiv : 2004.08037 . doi : 10.1145 / 3357713.3384248 . ISBN 9781450369794. S2CID 215814356 .
- ^ Garlík, Michal (2020). "Fallo de propiedad de disyunción factible para resolución k -DNF y dureza NP de automatizarla". ECCC . arXiv : 2003.10230 .
- ^ Beame, Paul ; Pitassi, Toniann (1996). "Límites inferiores de resolución simplificada y mejorada". 37º Simposio anual sobre los fundamentos de la informática : 274–282.
- ^ a b Ben-Sasson, Eli ; Wigderson, Avi (1999). "Las pruebas breves tienen una resolución limitada simplificada". Actas del 31º Simposio ACM sobre Teoría de la Computación . págs. 517–526.
- ^ Cook, Stephen (1975). "Pruebas factiblemente constructivas y el cálculo propositiona". Actas del Séptimo Simposio Anual ACM sobre Teoría de la Computación . págs. 83–97.
- ^ París, Jeff ; Wilkie, Alex (1985). "Contando problemas en aritmética acotada". Métodos en lógica matemática . Apuntes de clase en matemáticas. 1130 : 317–340. doi : 10.1007 / BFb0075316 . ISBN 978-3-540-15236-1.
- ^ Cook, Stephen ; Nguyen, Phuong (2010). Fundamentos lógicos de la complejidad de la prueba . Perspectivas en lógica. Cambridge: Cambridge University Press. doi : 10.1017 / CBO9780511676277 . ISBN 978-0-521-51729-4. Señor 2589550 .( borrador de 2008 )
- ^ a b Ajtai, M. (1988). "La complejidad del principio del casillero". Actas del 29º Simposio Anual de IEEE sobre la Fundación de las Ciencias de la Computación . págs. 346–355.
- ^ Haken, A. (1985). "La intratabilidad de la resolución". Informática Teórica . 39 : 297-308. doi : 10.1016 / 0304-3975 (85) 90144-6 .
- ^ Krajíček, Jan ; Pudlák, Pavel ; Woods, Alan (1995). "Un límite inferior exponencial al tamaño de la profundidad limitada Frege pruebas del principio de casillero". Estructuras y algoritmos aleatorios . 7 (1): 15–39. doi : 10.1002 / rsa.3240070103 .
- ^ Pitassi, Toniann ; Beame, Paul ; Impagliazzo, Russell (1993). "Límites inferiores exponenciales para el principio de casillero". Complejidad computacional . 3 (2): 97–308. doi : 10.1007 / BF01200117 . S2CID 1046674 .
- ^ Krajíček, Jan (1994). "Límites inferiores al tamaño de las pruebas proposicionales de profundidad constante". Revista de lógica simbólica . 59 (1): 73–86. doi : 10.2307 / 2275250 . JSTOR 2275250 .
- ^ a b Krajíček, Jan (1997). "Teoremas de interpolación, límites inferiores para sistemas de prueba y resultados de independencia para aritmética acotada". Revista de lógica simbólica . 62 (2): 69–83. doi : 10.2307 / 2275541 . JSTOR 2275541 .
- ^ a b Pudlák, Pavel (1997). "Límites inferiores para pruebas de resolución y planos de corte y cálculos monótonos". Revista de lógica simbólica . 62 (3): 981–998. doi : 10.2307 / 2275583 . JSTOR 2275583 .
- ^ Pudlák, Pavel (2003). "Sobre reducibilidad y simetría de pares NP disjuntos". Theor. Computación. Ciencia . 295 : 323–339. doi : 10.2307 / 2275583 . JSTOR 2275583 .
- ^ Hrubeš, Pavel (2007). "Límites inferiores para lógicas modales". Revista de lógica simbólica . 72 (3): 941–958. doi : 10.2178 / jsl / 1191333849 .
- ^ 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 .
- ^ Hrubeš, Pavel (2009). "Sobre longitudes de 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 .
Otras lecturas
- 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 la prueba , Perspectivas en la lógica, Cambridge: Cambridge University Press, doi : 10.1017 / CBO9780511676277 , ISBN 978-0-521-51729-4, MR 2589550( borrador de 2008 )
- Krajíček, Jan (1995), aritmética acotada, lógica proposicional y teoría de la complejidad , Cambridge University Press
- Krajíček, Jan (2005), "Proof Complexity" (PDF) , en Laptev, A. (ed.), Proceedings of the 4th European Congress of Mathematics , Zürich: European Mathematical Society, pp. 221-231, MR 2185746
- Krajíček, Jan, Proof Complexity , Cambridge University Press, 2019.
- Pudlák, Pavel (1998), "The lengths of proofs", en Buss, SR (ed.), Handbook of Proof Theory , Studies in Logic and the Foundations of Mathematics, 137 , Amsterdam: North-Holland, págs. 547–637 , doi : 10.1016 / S0049-237X (98) 80023-2 , MR 1640332
enlaces externos
- Prueba de complejidad
- Prueba de la complejidad de la lista de correo.