En lógica matemática , teoría de la complejidad computacional e informática , la teoría existencial de los reales es el conjunto de todas las oraciones verdaderas de la forma
dónde es una fórmula sin cuantificadores que incluye igualdades y desigualdades de polinomios reales . [1]
El problema de decisión para la teoría existencial de los reales es el problema de encontrar un algoritmo que decida, para cada fórmula, si es verdadera o falsa. De manera equivalente, es el problema de probar si un conjunto semialgebraico dado no está vacío. [1] Este problema de decisión es NP-difícil y se encuentra en PSPACE . [2] Por lo tanto, tiene la complejidad significativamente menor que Alfred Tarski 's cuantificador eliminación procedimiento para decidir declaraciones en la teoría de primer orden de los números reales sin la restricción a los cuantificadores existenciales. [1] Sin embargo, en la práctica, los métodos generales para la teoría de primer orden siguen siendo la opción preferida para resolver estos problemas. [3]
Muchos problemas naturales en la teoría de grafos geométricos , especialmente los problemas de reconocer grafos de intersección geométrica y enderezar los bordes de los dibujos de grafos con cruces , pueden resolverse traduciéndolos a instancias de la teoría existencial de los reales, y están completos para esta teoría. La clase de complejidad , que se encuentra entre NP y PSPACE, se ha definido para describir esta clase de problemas. [4]
Fondo
En lógica matemática , una teoría es un lenguaje formal que consta de un conjunto de oraciones escritas utilizando un conjunto fijo de símbolos. La teoría de primer orden de los campos cerrados reales tiene los siguientes símbolos: [5]
- las constantes 0 y 1,
- una colección contable de variables ,
- las operaciones de suma, resta, multiplicación y (opcionalmente) división,
- símbolos <, ≤, =, ≥,> y ≠ para comparaciones de valores reales,
- las conectivas lógicas ∧, ∨, ¬ y ⇔,
- paréntesis, y
- el cuantificador universal ∀ y el cuantificador existencial ∃
Una secuencia de estos símbolos forma una oración que pertenece a la teoría de primer orden de los reales si está gramaticalmente bien formada, todas sus variables están debidamente cuantificadas y (cuando se interpreta como una declaración matemática sobre los números reales ) es un verdadero declaración. Como mostró Tarski, esta teoría se puede describir mediante un esquema de axioma y un procedimiento de decisión que es completo y eficaz: para cada oración totalmente cuantificada y gramatical, la oración o su negación (pero no ambas) pueden derivarse de los axiomas. La misma teoría describe todos los campos cerrados reales , no solo los números reales. [6] Sin embargo, hay otros sistemas numéricos que estos axiomas no describen con precisión; en particular, la teoría definida de la misma manera para números enteros en lugar de números reales es indecidible , incluso para oraciones existenciales ( ecuaciones diofánticas ) por el teorema de Matiyasevich . [5] [7]
La teoría existencial de los reales es el subconjunto de la teoría de primer orden que consiste en oraciones en las que todos los cuantificadores son existenciales y aparecen antes que cualquiera de los otros símbolos. Es decir, es el conjunto de todas las oraciones verdaderas de la forma
dónde es una fórmula sin cuantificadores que incluye igualdades y desigualdades de polinomios reales . El problema de decisión para la teoría existencial de lo real es el problema algorítmico de probar si una oración dada pertenece a esta teoría; de manera equivalente, para las cadenas que pasan las comprobaciones sintácticas básicas (usan los símbolos correctos con la sintaxis correcta y no tienen variables no cuantificadas) es el problema de probar si la oración es una declaración verdadera sobre los números reales. El conjunto de n -tuplas de números reales para cual es verdadero se llama conjunto semialgebraico , por lo que el problema de decisión para la teoría existencial de los reales puede reformularse de manera equivalente como probar si un conjunto semialgebraico dado no está vacío. [1]
Al determinar la complejidad temporal de los algoritmos para el problema de decisión de la teoría existencial de los reales, es importante tener una medida del tamaño de la entrada. La medida más simple de este tipo es la longitud de una oración: es decir, el número de símbolos que contiene. [5] Sin embargo, para lograr un análisis más preciso del comportamiento de los algoritmos para este problema, es conveniente descomponer el tamaño de entrada en varias variables, separando el número de variables a cuantificar, el número de polinomios dentro la oración y el grado de estos polinomios. [8]
Ejemplos de
La proporción áurea puede definirse como la raíz del polinomio . Este polinomio tiene dos raíces, de las cuales solo una (la proporción áurea) es mayor que una. Por lo tanto, la existencia de la proporción áurea puede expresarse mediante la oración
Debido a que la proporción áurea existe, esta es una oración verdadera y pertenece a la teoría existencial de los reales. La respuesta al problema de decisión para la teoría existencial de los reales, dada esta oración como entrada, es el valor booleano verdadero.
La desigualdad de medias aritméticas y geométricas establece que, por cada dos números no negativos y , se cumple la siguiente desigualdad:
Como se indicó anteriormente, es una oración de primer orden sobre los números reales, pero una con cuantificadores universales en lugar de existenciales, y una que usa símbolos adicionales para la división, raíces cuadradas y el número 2 que no están permitidos en el primer orden. teoría de los reales. Sin embargo, al elevar ambos lados al cuadrado, se puede transformar en la siguiente declaración existencial que se puede interpretar como una pregunta si la desigualdad tiene contraejemplos:
La respuesta al problema de decisión para la teoría existencial de los reales, dada esta oración como entrada, es el valor booleano falso: no hay contraejemplos. Por tanto, esta oración no pertenece a la teoría existencial de los reales, a pesar de tener la forma gramatical correcta.
Algoritmos
El método de eliminación de cuantificadores de Alfred Tarski (1948) mostró que la teoría existencial de los reales (y más generalmente la teoría de primer orden de los reales) se puede resolver algorítmicamente, pero sin un límite elemental en su complejidad. [9] [6] El método de descomposición algebraica cilíndrica , de George E. Collins (1975), mejoró la dependencia del tiempo a doblemente exponencial , [9] [10] de la forma
dónde es el número de bits necesarios para representar los coeficientes en la oración cuyo valor se va a determinar, es el número de polinomios en la oración, es su grado total, y es el número de variables. [8] En 1988, Dima Grigoriev y Nicolai Vorobjov habían demostrado que la complejidad era exponencial en un polinomio de, [8] [11] [12]
y en una secuencia de artículos publicados en 1992 James Renegar mejorado este a una dependencia exponencial por separado en, [8] [13] [14] [15]
Mientras tanto, en 1988, John Canny describió otro algoritmo que también tiene una dependencia temporal exponencial, pero solo una complejidad espacial polinomial; es decir, demostró que el problema se podía solucionar en PSPACE . [2] [9]
La complejidad computacional asintótica de estos algoritmos puede ser engañosa, porque en la práctica solo se pueden ejecutar con entradas de tamaño muy pequeño. En una comparación de 1991, Hoon Hong estimó que el procedimiento doblemente exponencial de Collins podría resolver un problema cuyo tamaño se describe estableciendo todos los parámetros anteriores en 2, en menos de un segundo, mientras que los algoritmos de Grigoriev, Vorbjov y Renegar en cambio, tomaría más de un millón de años. [8] En 1993, Joos, Roy y Solernó sugirieron que debería ser posible hacer pequeñas modificaciones a los procedimientos de tiempo exponencial para hacerlos más rápidos en la práctica que la decisión algebraica cilíndrica, así como más rápidos en teoría. [16] Sin embargo, a partir de 2009, todavía era cierto que los métodos generales para la teoría de primer orden de los reales seguían siendo superiores en la práctica a los algoritmos exponenciales individuales especializados en la teoría existencial de los reales. [3]
Problemas completos
Varios problemas de complejidad computacional y teoría de grafos geométricos pueden clasificarse como completos para la teoría existencial de los reales. Es decir, todo problema en la teoría existencial de los reales tiene una reducción de varios uno en tiempo polinomial a una instancia de uno de estos problemas, y a su vez estos problemas son reducibles a la teoría existencial de los reales. [4] [17]
Varios problemas de este tipo se refieren al reconocimiento de gráficos de intersección de cierto tipo. En estos problemas, la entrada es un gráfico no dirigido ; el objetivo es determinar si las formas geométricas de una determinada clase de formas se pueden asociar con los vértices del gráfico de tal manera que dos vértices sean adyacentes en el gráfico si y solo si sus formas asociadas tienen una intersección no vacía. Los problemas de este tipo que son completos para la teoría existencial de los reales incluyen el reconocimiento de gráficas de intersección de segmentos de línea en el plano, [4] [18] [5] reconocimiento de gráficas de disco unitario , [19] y reconocimiento de gráficas de intersección de conjuntos convexos en el plano. [4]
Para los gráficos dibujados en el plano sin cruces, el teorema de Fáry establece que se obtiene la misma clase de gráficos planos independientemente de si los bordes del gráfico se dibujan como segmentos de línea recta o como curvas arbitrarias. Pero esta equivalencia no es válida para otros tipos de dibujos. Por ejemplo, aunque el número de cruces de un gráfico (el número mínimo de cruces en un dibujo con bordes arbitrariamente curvados) puede determinarse en NP, es completo para la teoría existencial de los reales determinar si existe un dibujo que alcance un determinado enlazado en el número de cruce rectilíneo (el número mínimo de pares de bordes que se cruzan en cualquier dibujo con bordes dibujados como segmentos de línea recta en el plano). [4] [20] También es completo para la teoría existencial de los reales probar si un gráfico dado se puede dibujar en el plano con bordes en línea recta y con un conjunto dado de pares de bordes como sus cruces, o de manera equivalente, si un El dibujo curvo con cruces se puede enderezar de manera que conserve sus cruces. [21]
Otros problemas completos para la teoría existencial de los reales incluyen:
- el problema de la galería de arte de encontrar el menor número de puntos desde los cuales todos los puntos de un polígono dado son visibles. [22]
- el problema de empaquetado de decidir si un conjunto dado de polígonos puede caber en un contenedor cuadrado dado. [23]
- reconocimiento de gráficas de unidad de distancia , y prueba de si la dimensión o dimensión euclidiana de una gráfica es como máximo un valor dado. [9]
- capacidad de estiramiento de las pseudolinas (es decir, dada una familia de curvas en el plano, determinando si son homeomorfas a una disposición de línea ); [4] [24] [25]
- satisfacibilidad tanto débil como fuerte de la lógica cuántica geométrica en cualquier dimensión fija> 2; [26]
- Intervalo de verificación del modelo Cadenas de Markov con respecto a los autómatas inequívocos [27]
- el problema algorítmico de Steinitz (dado un enrejado , determine si es el enrejado de la cara de un politopo convexo ), incluso cuando se restringe a politopos de 4 dimensiones; [28] [29]
- espacios de realización de disposiciones de determinados cuerpos convexos [30]
- varias propiedades de los equilibrios de Nash de los juegos multijugador [31] [32] [33]
- incrustar un complejo abstracto dado de triángulos y cuadriláteros en un espacio euclidiano tridimensional; [17]
- incrustar varios gráficos en un conjunto de vértices compartido en el plano para que todos los gráficos se dibujen sin cruces; [17]
- reconocer los gráficos de visibilidad de conjuntos de puntos planos; [17]
- (afín proyectivo o no trivial) satisfacibilidad de una ecuación entre dos términos sobre el producto cruzado ; [34]
- determinar el número de pendiente mínimo de un dibujo no cruzado de un gráfico plano ; [35]
- el problema de evaluación parcial para el lenguaje de consulta de matriz propia MATLANG +. [36]
- el problema de compleción de la matriz de rango bajo . [37]
Basado en esto, la clase de complejidad Se ha definido como el conjunto de problemas que tienen una reducción polinomial-temporal de muchos-uno a la teoría existencial de los reales. [4]
Referencias
- ^ a b c d Basu, Saugata; Pollack, Richard ; Roy, Marie-Françoise (2006), "Teoría existencial de los reales", Algoritmos en geometría algebraica real , algoritmos y computación en matemáticas, 10 (2ª ed.), Springer-Verlag, págs. 505–532, doi : 10.1007 / 3-540-33099-2_14 , ISBN 978-3-540-33098-1.
- ^ a b Canny, John (1988), "Algunos cálculos algebraicos y geométricos en PSPACE", Actas del Vigésimo Simposio Anual de ACM sobre Teoría de la Computación (STOC '88, Chicago, Illinois, EE. UU.) , Nueva York, NY, EE. UU .: ACM, págs. . 460–467, doi : 10.1145 / 62212.62257 , ISBN 0-89791-264-0, S2CID 14535463
- ^ a b Passmore, Grant Olney; Jackson, Paul B. (2009), "Técnicas de decisión combinadas para la teoría existencial de los reales", Matemáticas informáticas inteligentes: 16º Simposio, Calculemus 2009, 8ª Conferencia Internacional, MKM 2009, Celebrada como parte del CICM 2009, Grand Bend, Canadá , 6-12 de julio de 2009, Proceedings, Part II , Lecture Notes in Computer Science , 5625 , Springer-Verlag, págs. 122-137, doi : 10.1007 / 978-3-642-02614-0_14.
- ^ a b c d e f g Schaefer, Marcus (2010), "Complejidad de algunos problemas geométricos y topológicos" (PDF) , Dibujo de gráficos, 17th International Symposium, GD 2009, Chicago, IL, EE. UU., Septiembre de 2009, Revised Papers , Lecture Notes in Computer Science, 5849 , Springer-Verlag, págs. 334–344, doi : 10.1007 / 978-3-642-11805-0_32.
- ^ a b c d Matoušek, Jiří (2014), "Gráficos de intersección de segmentos y", arXiv : 1406,2636 [ cs.CG ]
- ^ a b Tarski, Alfred (1948), A Decision Method for Elementary Algebra and Geometry , RAND Corporation, Santa Monica, Calif., MR 0028796.
- ^ Matiyasevich, Yu. V. (2006), "El décimo problema de Hilbert: ecuaciones diofánticas en el siglo XX", Eventos matemáticos del siglo XX , Berlín: Springer-Verlag, págs. 185-213, Bibcode : 2006metc.book ..... A , doi : 10.1007 / 3-540-29462-7_10 , MR 2182785.
- ^ a b c d e Hong, Hoon (11 de septiembre de 1991), Comparación de varios algoritmos de decisión para la teoría existencial de la realidad , Informe técnico, 91–41, RISC Linz[ enlace muerto permanente ] .
- ^ a b c d Schaefer, Marcus (2013), "Realizability of graphs and linkages", en Pach, János (ed.), Thirty Essays on Geometric Graph Theory , Springer-Verlag, págs. 461–482, doi : 10.1007 / 978-1-4614 -0110-0_24.
- ^ Collins, George E. (1975), "Eliminación del cuantificador para campos cerrados reales por descomposición algebraica cilíndrica", Teoría de los autómatas y lenguajes formales (Second GI Conf., Kaiserslautern, 1975) , Lecture Notes in Computer Science , 33 , Berlín: Springer- Verlag, págs. 134-183, MR 0403962.
- ^ Grigor'ev, D. Yu. (1988), "Complejidad de decidir el álgebra de Tarski", Journal of Symbolic Computation , 5 (1-2): 65-108, doi : 10.1016 / S0747-7171 (88) 80006-3 , MR 0949113.
- ^ Grigor'ev, D. Yu. ; Vorobjov, NN, Jr. (1988), "Resolver sistemas de desigualdades polinómicas en tiempo subexponencial" (PDF) , Journal of Symbolic Computation , 5 (1–2): 37–64, doi : 10.1016 / S0747-7171 (88) 80005-1 , MR 0949112.
- ^ Renegar, James (1992), "Sobre la complejidad computacional y la geometría de la teoría de primer orden de los reales. I. Introducción. Preliminares. La geometría de los conjuntos semi-algebraicos. El problema de decisión para la teoría existencial de los reales", Journal of Symbolic Computation , 13 (3): 255–299, doi : 10.1016 / S0747-7171 (10) 80003-3 , MR 1156882.
- ^ Renegar, James (1992), "Sobre la complejidad computacional y la geometría de la teoría de primer orden de los reales. II. El problema de decisión general. Preliminares para la eliminación de cuantificadores", Journal of Symbolic Computation , 13 (3): 301-327 , doi : 10.1016 / S0747-7171 (10) 80004-5 , MR 1156883.
- ^ Renegar, James (1992), "Sobre la complejidad computacional y la geometría de la teoría de primer orden de los reales. III. Eliminación del cuantificador", Journal of Symbolic Computation , 13 (3): 329–352, doi : 10.1016 / S0747- 7171 (10) 80005-7 , MR 1156884.
- ^ Heintz, Joos; Roy, Marie-Françoise ; Solernó, Pablo (1993), "Sobre la complejidad teórica y práctica de la teoría existencial de los reales", The Computer Journal , 36 (5): 427–431, doi : 10.1093 / comjnl / 36.5.427 , MR 1234114.
- ^ a b c d Cardinal, Jean (diciembre de 2015), "Computational geometry column 62", SIGACT News , 46 (4): 69–78, arXiv : cs / 0010039 , doi : 10.1145 / 2852040.2852053 , S2CID 17276902.
- ^ Kratochvíl, Jan ; Matoušek, Jiří (1994), "Gráficos de intersección de segmentos", Journal of Combinatorial Theory, Serie B , 62 (2): 289–315, doi : 10.1006 / jctb.1994.1071 , MR 1305055.
- ^ Kang, Ross J .; Müller, Tobias (2011), "Representaciones de gráficos en esferas y productos escalares ", Actas del Vigésimo Séptimo Simposio Anual sobre Geometría Computacional (SCG'11), 13-15 de junio de 2011, París, Francia , págs. 308-314.
- ^ Bienstock, Daniel (1991), "Algunos problemas de cruces numéricos demostrablemente difíciles", Geometría discreta y computacional , 6 (5): 443–459, doi : 10.1007 / BF02574701 , MR 1115102 , S2CID 38465081.
- ^ Kynčl, Jan (2011), "Realización simple de gráficos topológicos abstractos completos en P", Geometría discreta y computacional , 45 (3): 383–399, doi : 10.1007 / s00454-010-9320-x , MR 2770542 , S2CID 12419381.
- ^ Abrahamsen, Mikkel; Adamaszek, Anna; Miltzow, Tillmann (2018), "El problema de la galería de arte es-complete ", en Diakonikolas, Ilias; Kempe, David; Henzinger, Monika (eds.), Actas del 50 ° Simposio Anual ACM SIGACT sobre Teoría de la Computación, STOC 2018, Los Ángeles, CA, EE. UU., 25-29 de junio de 2018 , ACM, págs. 65–73, arXiv : 1704.06969 , doi : 10.1145 / 3188745.3188868
- ^ Abrahamsen, Mikkel; Miltzow, Tillmann; Seiferth, Nadja (2020), "Marco para-completeness of bidimensional empaquetados ", 61º Simposio Anual de IEEE sobre Fundamentos de las Ciencias de la Computación, FOCS 2020, Durham, NC, EE. UU., 16-19 de noviembre de 2020 , IEEE, págs. 1014–1021, arXiv : 2004.07558 , doi : 10.1109 / FOCS46700.2020.00098
- ^ Mnëv, NE (1988), "Los teoremas de universalidad sobre el problema de clasificación de las variedades de configuración y las variedades de politopos convexos", Topología y geometría — Seminario Rohlin , Lecture Notes in Mathematics , 1346 , Berlín: Springer-Verlag, págs. 527–543, doi : 10.1007 / BFb0082792 , MR 0970093.
- ^ Shor, Peter W. (1991), "Stretchability of pseudolines is NP-hard", Geometría aplicada y matemáticas discretas , Serie DIMACS en matemáticas discretas y ciencias de la computación teórica, 4 , Providence, RI: American Mathematical Society , págs. 531–554 , MR 1116375.
- ^ Herrmann, Christian; Ziegler, Martin (2016), "Complejidad computacional de la satisfacción cuántica", Journal of the ACM , 63 , arXiv : 1004.1696 , doi : 10.1145 / 2869073 , S2CID 2253943.
- ^ Benedikt, Michael; Lenhardt, Rastislav; Worrell, James (2013), "Verificación del modelo LTL de cadenas de Markov a intervalos", Herramientas y algoritmos para la construcción y análisis de sistemas. TACAS 2013 , Lecture Notes in Computer Science, 7795 , págs. 32–46, doi : 10.1007 / 978-3-642-36742-7_3
- ^ Björner, Anders ; Las Vergnas, Michel ; Sturmfels, Bernd ; White, Neil; Ziegler, Günter M. (1993), Oriented Matroids , Encyclopedia of Mathematics and its Applications, 46 , Cambridge: Cambridge University Press, Corolario 9.5.10, p. 407, ISBN 0-521-41836-4, MR 1226888.
- ^ Richter-Gebert, Jürgen; Ziegler, Günter M. (1995), "Los espacios de realización de 4 politopos son universales", Boletín de la Sociedad Americana de Matemáticas , Nueva Serie, 32 (4): 403–412, arXiv : math / 9510217 , Bibcode : 1995math .. ... 10217R , doi : 10.1090 / S0273-0979-1995-00604-X , MR 1316500 , S2CID 7940964.
- ^ Dobbins, Michael Gene; Holmsen, Andreas; Hubard, Alfredo (2017), "Espacios de realización de arreglos de cuerpos convexos", Geometría discreta y computacional , 58 (1): 1–29, arXiv : 1412.0371 , doi : 10.1007 / s00454-017-9869-8 , MR 3658327 , S2CID 39856606.
- ^ Garg, Jugal; Mehta, Ruta; Vazirani, Vijay V .; Yazdanbod, Sadra (2015), "ETR-Completitud para versiones de decisión de equilibrios de Nash (simétricos) multijugador", Proc. 42o Coloquio Internacional sobre Autómatas, Lenguajes y Programación (ICALP) , Lecture Notes in Computer Science, 9134 , Springer, págs. 554–566, doi : 10.1007 / 978-3-662-47672-7_45.
- ^ Bilo, Vittorio; Mavronicolas, Marios (2016), "Un catálogo de problemas de decisión completos de ETR sobre los equilibrios de Nash en juegos para varios jugadores", Actas del 33 ° Simposio internacional sobre aspectos teóricos de la informática , LIPIcs, Schloss Dagstuhl - Leibnitz Zentrum fuer Informatik, págs. .17 : 1–17: 13, doi : 10.4230 / LIPIcs.STACS.2016.17.
- ^ Bilo, Vittorio; Mavronicolas, Marios (2017), "ETR-Complete Decision Problems about Symmetric Nash Equilibria in Symmetric Multi-Player Games", Actas del 34 ° Simposio internacional sobre aspectos teóricos de la informática , LIPIcs, Schloss Dagstuhl - Leibnitz Zentrum fuer Informatik, págs. 13: 1–13: 14.
- ^ Herrmann, Christian; Sokoli, Johanna; Ziegler, Martin (2013), "La satisfacción de los términos de productos cruzados es completa para las máquinas reales de Blum-Shub-Smale de tiempo polimétrico no determinista", Actas de la 6ª Conferencia sobre Máquinas, Computaciones y Universalidad (MCU'13) , 128 , doi : 10.4204 / EPTCS.128 , S2CID 2151889.
- ^ Hoffmann, Udo (2016), "El número de pendiente plana", Actas de la 28ª Conferencia Canadiense sobre Geometría Computacional (CCCG 2016).
- ^ Brijder, Robert; Geerts, Floris; Van den Bussche, Jan; Weerwag, Timmy (2019), "Sobre el poder expresivo de los lenguajes de consulta para matrices". , Transacciones de ACM en sistemas de base de datos , ACM, 44 (4): 15: 1–15: 31, doi : 10.1145 / 3331445 , S2CID 204714822.
- ^ Bertsimas, Dimitris; Cory-Wright, Ryan; Pauphilet, Jean (2020), "Optimización cónica de proyección mixta: un nuevo paradigma para modelar restricciones de rango", arXiv : 2009.10395 [ math.OC ].