Los científicos informáticos y matemáticos de la Universidad Carnegie Mellon han resuelto el último, pieza obstinada de la conjetura de Keller, un problema de geometría sobre el que los científicos han estado desconcertados durante 90 años.

Al estructurar el rompecabezas como lo que los científicos de la computación llaman un problema de satisfacibilidad, los investigadores resolvieron el problema con cuatro meses de frenética programación de computadoras y solo 30 minutos de computación usando un grupo de computadoras.

"Me alegré mucho cuando lo resolvimos, pero luego me entristeció un poco que el problema desapareciera, "dijo John Mackey, un profesor de enseñanza en el Departamento de Ciencias de la Computación (CSD) y el Departamento de Ciencias Matemáticas que había seguido la conjetura de Keller desde que era un estudiante de posgrado hace 30 años. "Pero luego me sentí feliz de nuevo. Sólo hay un sentimiento de satisfacción".

La solución fue otro éxito más para un enfoque iniciado por Marijn Heule, profesor asociado de informática que se incorporó al CSD el pasado mes de agosto. Heule ha utilizado un solucionador de SAT, un programa de computadora que usa lógica proposicional para resolver problemas de satisifiability (SAT), para superar varios desafíos matemáticos antiguos, incluyendo el problema de las triples pitagóricas y el número de Schur 5.

"El problema ha intrigado a muchas personas durante décadas, casi un siglo, Heule dijo sobre la conjetura de Keller:"Esto es realmente un escaparate de lo que se puede hacer ahora que no era posible antes".

La conjetura planteado por el matemático alemán Eduard Ott-Heinrich Keller, tiene que ver con el mosaico, específicamente, cómo cubrir un área con mosaicos del mismo tamaño sin espacios ni superposición. La conjetura es que al menos dos de los mosaicos tendrán que compartir un borde y que esto es cierto para espacios de todas las dimensiones.

Es fácil demostrar que es cierto para baldosas bidimensionales y cubos tridimensionales. A partir de 1940, la conjetura había demostrado ser cierta para todas las dimensiones hasta seis. En 1990, sin embargo, Los matemáticos demostraron que no funciona en la dimensión 10 o superior.

Fue entonces cuando la conjetura de Keller capturó la imaginación de Mackey, luego estudiante de la Universidad de Hawaii. Con una oficina junto al clúster de computación de la universidad, estaba intrigado porque el problema se podía traducir, usando la teoría de grafos discretos, en una forma que las computadoras puedan explorar. Ene sta forma, llamado gráfico de Keller, los investigadores podrían buscar "camarillas":subconjuntos de elementos que se conectan sin compartir una cara, refutando así la conjetura.

En 2002, Mackey hizo precisamente eso, descubriendo una camarilla en la dimensión ocho. Al hacerlo, demostró que la conjetura falla en esa dimensión y, por extensión, en dimensión nueve.

Eso dejó la conjetura sin resolver para la dimensión siete.

Cuando Heule llegó a CMU de la Universidad de Texas el año pasado, ya tenía la reputación de usar el solucionador SAT para resolver problemas matemáticos abiertos de larga data.

"Pensé, tal vez podamos usar su técnica, "Recordó Mackey. En poco tiempo, comenzó a discutir cómo usar el solucionador SAT en la conjetura de Keller con Heule y Joshua Brakensiek, una doble especialización en ciencias matemáticas y ciencias de la computación que ahora está cursando un doctorado. en ciencias de la computación en la Universidad de Stanford.

Un solucionador de SAT requiere estructurar el problema usando una fórmula proposicional:(A o no B) y (B o C), etc., de modo que el solucionador puede examinar todas las variables posibles en busca de combinaciones que satisfagan todas las condiciones.

"Hay muchas formas de realizar estas traducciones, y la calidad de la traducción por lo general hace o rompe su capacidad para resolver el problema, "Dijo Heule.

Con 15 años de experiencia, Heule es experta en realizar estas traducciones. Uno de sus objetivos de investigación es desarrollar un razonamiento automatizado para que esta traducción se pueda realizar automáticamente, permitiendo que más personas utilicen estas herramientas en sus problemas.

Incluso con una traducción de alta calidad, el número de combinaciones a comprobar en la dimensión siete era asombroso —un número con 324 dígitos— sin una solución a la vista ni siquiera con una supercomputadora. Pero Heule y los demás aplicaron una serie de trucos para reducir el tamaño del problema. Por ejemplo, si una configuración de datos resultó inviable, podrían rechazar automáticamente otras combinaciones que se basen en él. Y dado que muchos de los datos eran simétricos, el programa podría descartar imágenes espejo de una configuración si llegara a un callejón sin salida en una disposición.

Usando estas técnicas, redujeron su búsqueda a aproximadamente mil millones de configuraciones. A ellos se unieron en este esfuerzo David Narváez, un doctorado estudiante en el Instituto de Tecnología de Rochester, quien fue investigador visitante en el otoño de 2019.

Una vez que ejecutaron su código en un grupo de 40 computadoras, finalmente tuvieron una respuesta:la conjetura es cierta en la dimensión siete.

"La razón por la que lo logramos es que John tiene décadas de experiencia y conocimiento de este problema y pudimos transformarlo en una búsqueda generada por computadora, "Dijo Heule.

La prueba del resultado es calculada completamente por la computadora, Heule dijo:a diferencia de muchas publicaciones que combinan partes de una prueba verificadas por computadora con redacciones manuales de otras partes. Eso dificulta que los lectores comprendan El lo notó. La prueba informática de la solución Keller incluye todos los aspectos de la solución, incluyendo una parte que rompe la simetría aportada por Narváez, Heule enfatizó, de modo que ningún aspecto de la prueba necesita depender del esfuerzo manual.

"Podemos tener una confianza real en la exactitud de este resultado, ", dijo. Un documento que describe la resolución de Heule, Mackey, Brakensiek y Narvaez ganaron el premio al mejor artículo en la Conferencia conjunta internacional sobre razonamiento automatizado en junio.

Resolver la conjetura de Keller tiene aplicaciones prácticas, Dijo Mackey. Esas camarillas que los científicos buscan para refutar la conjetura son útiles para generar códigos no lineales que pueden acelerar la transmisión de datos. Por tanto, el solucionador SAT se puede utilizar para encontrar códigos no lineales de mayor dimensión de lo que era posible anteriormente.

Heule propuso recientemente usar el solucionador SAT para abordar un problema matemático aún más famoso:la conjetura de Collatz. En este problema, la idea es elegir cualquier número entero positivo y dividir por 2 si es un número par o multiplicar por 3 y sumar 1 si es un número impar. Luego aplique las mismas reglas al número resultante y a cada resultado sucesivo. La conjetura es que el resultado final siempre será 1.

Resolver Collatz con el solucionador SAT "es una posibilidad remota, ", Reconoció Heule. Pero es un objetivo ambicioso, añadió, explicando que el solucionador de SAT podría usarse para resolver una serie de problemas matemáticos menos intimidantes, incluso si Collatz resulta inalcanzable.