Noticias #eXplora <a href="https://static1.abc.es/media/ciencia/2020/10/08/khguy-kSrH--620x349@abc.jpg">Media</a>En matemáticas, una conjetura es una afirmación que debe ser demostrada para ser irrefutable. Es decir, se plantea y después se comprueba. Una de estas conjeturas es la de Keller, cuyo enunciado afirma que «un plano no puede ser cubierto completamente con cuadrados idénticos sin solaparse sin que al menos dos de ellos compartan uno de sus lados». Hasta ahora se había demostrado para todos los números. Sin embargo, el 7 llevaba casi un siglo desconcertando a los científicos. Pero uniendo matemáticas e informática, cuatro meses de frenética programación y 30 minutos de computación, por fin se ha conseguido hallar la última pieza del rompecabezas: la demostración de la conjetura de Keller. 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 de las baldosas 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. Reducir las posibilidades a tan solo mil millones 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…