La poderosa tecnología de resolución de SAT puede funcionar con la infame hipótesis de Collatz. Sin embargo, las posibilidades de que esto ocurra no son muy altas.
En los últimos años, Mariin Hijul ha utilizado una tecnología de búsqueda de pruebas computarizada llamada SAT solver (SAT para satisfacer) para conquistar una impresionante lista de problemas matemáticos. Trillizos pitagóricos en 2016, el número 5 de Schur en 2017, y recientemente la hipótesis de Keller en la séptima dimensión, sobre la que escribimos no hace mucho en el artículo " La búsqueda por computadora ayudó a resolver un problema matemático de 90 años ".
Ahora, sin embargo, Hijul, un informático de la Universidad Carnegie Mellon, se ha fijado en un objetivo aún más ambicioso: la conjetura de Collatz, considerada por muchos como el problema abierto más difícil de las matemáticas (y posiblemente el más simple de formular). Otros matemáticos, al enterarse por mí de que Khiyul estaba haciendo tal intento, se mostraron escépticos al respecto.
"No veo cómo este problema se puede resolver por completo con el solucionador SAT", dijo Thomas Hales de la Universidad de Pittsburgh, un destacado experto en evidencia informática. Esta tecnología esencialmente ayuda a los matemáticos a resolver problemas, algunos de los cuales tienen un número infinito de opciones, convirtiéndolos en problemas finitos y discretos.
Sin embargo, Hales, como los demás, temía subestimar a Khiyul. “Es muy bueno para encontrar formas inteligentes de formular problemas en el lenguaje SAT. Es muy bueno en eso ".
Scott Aaronsonde la Universidad de Texas en Austin, trabajando con Hiyul en la conjetura de Collatz, agregó: “Marin es un hombre con un martillo, es decir, con un solucionador de SAT, y es probablemente el portador más digno de este martillo en todo el mundo. Y trata de aplicarlo a casi todo ". Pero solo el tiempo dirá si puede convertir la hipótesis de Collatz en un clavo.
La solución SAT requiere reformular los problemas en un lenguaje comprensible por computadora que usa lógica proposicional , y luego conectar computadoras para decidir si hay una manera de hacer que esas declaraciones sean verdaderas. He aquí un ejemplo sencillo.
Digamos que usted es un padre que intenta organizar el cuidado de sus hijos. Una de sus niñeras puede trabajar toda la semana excepto los martes y jueves. El otro es aparte de martes y viernes. El tercero, excepto jueves y viernes. Debe sentarse con su hijo los martes, jueves y viernes. ¿Se puede lograr esto?
Una forma de probar esto es convertir las restricciones de niñera en una fórmula y enviarla al solucionador de SAT. El programa buscará una forma de distribuir los días entre las niñeras para que la fórmula resulte verdadera, o “satisfecha”, es decir, para obtener los tres días que necesita. Si tiene éxito, tal método existirá.
Desafortunadamente, no está claro de inmediato cómo reformular muchas de las preguntas matemáticas más importantes en el lenguaje SAT. Pero a veces pueden reformularse como preguntas de satisfacción de formas inesperadas.
"Es difícil predecir cuándo se reducirá la tarea a un cálculo enorme pero finito", dijo Aaronson.
La conjetura de Collatz es una de esas preguntas matemáticas que al principio no parece un problema de niñera. Ella sugiere lo siguiente: tome cualquier número (entero, distinto de cero). Si es impar, multiplíquelo por 3 y sume 1. Si es par, divida por 2. Como resultado, obtendrá un nuevo número. Aplíquele las mismas reglas y continúe. La hipótesis predice que, independientemente del número inicial, terminas con 1 y luego te quedas atascado en un bucle: 1, 4, 2, 1.
Y, a pesar de que esta hipótesis se ha trabajado durante casi 100 años, los matemáticos no se han acercado a probarla.
Pero esto no detuvo a Khiyul. En 2018, él y Aronson, mientras eran colegas universitarios, recibieron una subvención de la National Science Foundation para aplicar el solucionador SAT a la conjetura de Collatz.
Toma cualquier número. Si es impar, multiplíquelo por 3 y sume 1. Si es par, divida por 2. Como resultado, obtendrá un nuevo número. Aplíquele las mismas reglas y continúe. ¿Puedes encontrar un número que no conduzca a 1? Puede probarlo usted mismo .
Para empezar, Aaronson, un científico de la computación, propuso una formulación alternativa de la hipótesis de Collatz, la llamada. Un "sistema de reglas de sustitución" que facilitó el trabajo de las computadoras.
En un sistema de reglas de sustitución, trabaja con un conjunto de caracteres, como las letras A, B y C. Las usa para formar secuencias: ACACBACB. También tiene reglas para convertir estas secuencias. Una regla puede decir que cuando conoces un AC, lo reemplazas con BC. Otros pueden reemplazar el avión con AAA. Puede definir cualquier número de reglas que definan cualquier transformación.
Los informáticos generalmente necesitan saber si una determinada JV siempre termina. Es decir, independientemente de con qué línea comenzar y en qué orden aplicar las reglas, ¿es cierto que la línea eventualmente se convertirá en un estado en el que no se pueden aplicar reglas?
Aaronson ideó un SP con siete símbolos y 11 reglas, similar a la hipótesis de Collatz. Si pueden demostrar que su JV siempre termina, de ese modo probarán que la hipótesis es correcta.
Para convertir la conjetura de Collatz en un problema de resolución de SAT, Aaronson y Hiyul tuvieron que dar otro paso que involucraba matrices o arreglos de números. Necesitaban asignar una matriz única a cada símbolo en su SP. Este enfoque, una forma común de buscar pruebas de que el SP está terminando el trabajo, les permitiría razonar sobre las transformaciones numéricas a través de la multiplicación de matrices. Siete matrices que denotan siete símbolos con SP tenían que satisfacer un conjunto completo de restricciones, reflejando la correspondencia de 11 reglas entre sí.
"Primero, intente encontrar matrices que satisfagan estas restricciones", dijoEmre Yolchu , estudiante de doctorado en la Universidad Carnegie Mellon, trabajando en este problema con Hijul. “Si tienes éxito, pruebas que la ejecución se detiene”, y por tanto que la hipótesis de Collatz es correcta.
El solucionador SAT puede responder a la pregunta de la existencia de matrices que satisfagan estas restricciones. Aaronson y Hijul primero ejecutaron el solucionador SAT en pequeñas matrices 2x2. No encontraron opciones de trabajo. Luego probaron matrices de 3x3. Y de nuevo en vano. Continuaron aumentando el tamaño de las matrices con la esperanza de poder encontrarlas.
Sin embargo, este enfoque no puede evolucionar indefinidamente, ya que la complejidad de buscar matrices adecuadas crece exponencialmente con su tamaño. Hijul sugiere que las computadoras modernas simplemente no pueden manejar matrices mayores de 12x12.
“Cuando las matrices se vuelven demasiado complejas, no se puede resolver el problema”, dijo.
Hijul todavía está trabajando para optimizar la búsqueda, tratando de hacerla más eficiente para que el solucionador SAT pueda verificar matrices cada vez más grandes. Ella y sus colegas están trabajando en un artículo que resuma sus descubrimientos actuales, pero están casi sin ideas y probablemente tendrán que rendirse pronto, al menos por un tiempo.
Después de todo, el atractivo del solucionador de SAT es que si solo pudiera averiguar cómo verificar otro caso, llamar a otra niñera, extender la búsqueda incluso por un tiempo, probablemente podría encontrar lo que estaba buscando. En este sentido, la principal ventaja de Khiyul puede que no sea su experiencia con los solucionadores de SAT, sino su amor por la búsqueda de resultados.
"Soy simplemente un optimista", dijo. "A menudo siento que tengo suerte, así que trato de ver hasta dónde puedo llegar".