Resuelven un misterio geométrico de casi un siglo de antigüedad

El equipo recurrió a un solucionador de SAT, -un programa de ordenador que usa lógica proposicional para resolver problemas de satisfaciblidad (SAT)-, que ya sirvió para superar varios desafíos matemáticos antiguos como el problema de triples de Pitágoras y la Factorización de Schur.

«El problema ha intrigado a muchas personas durante décadas, casi un siglo», afirma en un comunicado el autor principal del hallazgo y profesor de ciencias de la computación, Marijn Heule . «Pero esto es realmente una pequeña muestra de todo lo que se puede hacer ahora que antes no era posible».

La conjetura, planteada por el matemático alemán Eduard Ott-Heinrich Keller , tiene que ver con las baldosas. Específicamente, cómo cubrir un área con baldosas del mismo tamaño sin ningún espacio o 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 se cumple para los mosaicos bidimensionales y los cubos tridimensionales. En 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 llamó la atención del profesor de Matemáticas John Mackey -y coautor del descubrimiento- , entonces estudiante de la Universidad de Hawai. Estaba intrigado porque el problema podía traducirse, utilizando la teoría de grafos discretos, a una forma que los ordenadores pudieran explorar.

En esta forma, llamada gráfica 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 consiguió descubrir una camarilla en la dimensión ocho. Al hacerlo, demostró que la conjetura falla en esa dimensión y, por extensión, en la dimensión nueve. Pero la siete se quedó sin respuesta.

Cuando Heule llegó a la Universidad de Texas el año pasado, ya había usado el solucionador SAT para resolver los problemas matemáticos pendientes. Un solucionador de SAT requiere estructurar el problema usando una fórmula proposicional (A o no B) y (B o C), etc., para que el solucionador pueda examinar todas las variables posibles para combinaciones que satisfagan todas las condiciones.

«Hay muchas formas de hacer estas traducciones, y la calidad de la traducción, por lo general, hace o rompe su capacidad para resolver el problema», afirma Heule. Con 15 años de experiencia, Heule es experto en realizar estas traducciones. Uno de los objetivos de su investigación es desarrollar un razonamiento automatizado para que esta traducción se pueda realizar automáticamente, permitiendo que más y más personas utilicen estas herramientas en sus problemas.

Incluso con una traducción de alta calidad, la cantidad de combinaciones a verificar en la dimensión siete era demasiado grande-un número con 324 dígitos- con una solución que no se veía por ninguna parte, incluso 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 basaran en ella. Y dado que muchos de los datos eran simétricos, el programa podía descartar imágenes espejo de una configuración si llegaba a un callejón sin salida en una disposición.

Usando estas técnicas, redujeron su búsqueda a aproximadamente 1.000 millones de configuraciones. Un número que, aunque pueda parecer muy grande, puede ser procesado por los nuevos ordenadores. 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.

«Me alegré mucho cuando lo resolvimos, pero luego me entristeció un poco que el problema desapareciera», afirma Mackey . «Pero luego me sentí feliz de nuevo. Solo hay un sentimiento de satisfacción». «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», asegura por su parte Heule.

Resolver la conjetura de Keller tiene aplicaciones prácticas: esas «camarillas» 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», reconoce Heule. Pero es una meta a la que aspira.