Una prueba asistida por computadora resuelve el problema de ‘colorear el empaque’


Heule, sin embargo, encontró estimulante el descubrimiento de resultados pasados. Demostró que otros investigadores encontraron el problema lo suficientemente importante como para trabajar en él, y le confirmó que el único resultado que valía la pena obtener era resolver el problema por completo.

“Una vez que nos dimos cuenta de que había habido 20 años de trabajo en el problema, eso cambió completamente la imagen”, dijo.

Evitando lo vulgar

A lo largo de los años, Heule había hecho carrera encontrando formas eficientes de buscar entre vastas combinaciones posibles. Su enfoque se llama resolución SAT, abreviatura de «satisfacibilidad». Implica construir una fórmula larga, llamada fórmula booleana, que puede tener dos resultados posibles: 0 o 1. Si el resultado es 1, la fórmula es verdadera y el problema está satisfecho.

Para el problema de coloración del empaquetamiento, cada variable en la fórmula podría representar si una celda determinada está ocupada por un número determinado. Una computadora busca formas de asignar variables para satisfacer la fórmula. Si la computadora puede hacerlo, sabrá que es posible empaquetar la cuadrícula en las condiciones que ha establecido.

Desafortunadamente, una codificación sencilla del problema del color del empaque como una fórmula booleana podría extenderse a muchos millones de términos: una computadora, o incluso una flota de computadoras, podría funcionar para siempre probando todas las diferentes formas de asignar variables dentro de ella.

“Tratar de hacer esta fuerza bruta tomaría hasta que el universo termine si lo hicieras ingenuamente”, dijo Goddard. «Así que necesitas algunas simplificaciones geniales para reducirlo a algo que sea incluso posible».

Además, cada vez que agregas un número al problema de coloración del empaque, se vuelve unas 100 veces más difícil, debido a la forma en que se multiplican las posibles combinaciones. Esto significa que si un banco de computadoras trabajando en paralelo pudiera descartar 12 en un solo día de cómputo, necesitarían 100 días de tiempo de cómputo para descartar 13.

Heule y Subercaseaux consideraban que escalar un enfoque computacional de fuerza bruta era vulgar, en cierto modo. “Teníamos varias ideas prometedoras, por lo que adoptamos la mentalidad de ‘Intentemos optimizar nuestro enfoque hasta que podamos resolver este problema en menos de 48 horas de computación en el clúster’”, dijo Subercaseaux.

Para hacer eso, tuvieron que idear formas de limitar la cantidad de combinaciones que el clúster de computación tenía que probar.

“[They] no solo quiero resolverlo, sino resolverlo de una manera impresionante”, dijo Alexander Soifer de la Universidad de Colorado, Colorado Springs.

Heule y Subercaseaux reconocieron que muchas combinaciones son esencialmente iguales. Si está tratando de llenar un mosaico en forma de diamante con ocho números diferentes, no importa si el primer número que coloca es uno arriba y uno a la derecha del cuadrado central, o uno abajo y uno a la izquierda de la plaza del centro. Las dos ubicaciones son simétricas entre sí y restringen su próximo movimiento exactamente de la misma manera, por lo que no hay razón para verificarlas a ambas.

Si todos los problemas de empaquetamiento pudieran resolverse con un patrón de tablero de ajedrez, donde una cuadrícula diagonal de 1 cubre todo el espacio (como los espacios oscuros en un tablero de ajedrez), los cálculos podrían simplificarse enormemente. Sin embargo, ese no es siempre el caso, como en este ejemplo de un mosaico finito con 14 números. El patrón del tablero de ajedrez debe romperse en algunos lugares hacia la parte superior izquierda.Cortesía de Bernardo Subercaseaux y Marijn Heule



Source link-46