Métodos exactos
Solucionadores capaces de demostrar: codificaciones SAT y CSP, programación entera y sus relajaciones, cobertura exacta, encuentro en el medio y mapas de proyección iterados. Los métodos completos se atascan en el tablero completo, pero sus veredictos se ganan su lugar como pruebas de imposibilidad en subtableros.
Eternity II se formula limpiamente como un problema de cobertura exacta, y el algoritmo X de Knuth con enlaces danzantes es la máquina clásica para ellos. Dónde brilla de verdad (tableros pequeños, conteo exhaustivo) y las dos razones por las que no vence al 16×16: un árbol de búsqueda que nunca se reduce, y ningún crédito parcial.
Enumerar dos mitades de un problema y unirlas en una interfaz compartida, intercambiando memoria por un exponente reducido a la mitad. El truco clásico de Horowitz–Sahni, qué aspecto tiene sobre bandas del tablero, y qué midió el experimento BANDSAW de este proyecto, incluido el método unilateral que lo superó.
Un tablero parcial fuerte es una región superior que el productor trabajó más una banda inferior de filas sin terminar. Se congela la parte alta, se entrega la cola a un solucionador de restricciones exacto y se lee qué mitad fija el techo: la estructura del productor o el final de partida abaratado.
Escribir el puzzle como cláusulas y entregárselo a un solucionador industrial: el movimiento evidente, intentado desde 2008. Por qué los solucionadores completos se atascan en el tablero completo, y dónde sus veredictos siguen ganándose el sustento como pruebas de imposibilidad.
Escribe Eternity II como un programa entero, abandona la integralidad, y un solucionador lineal alcanza error cero en segundos, con un 30 % de una pieza y un 20 % de otra compartiendo una esquina. Dieciocho años de campañas comunitarias midieron dónde termina la comodidad fraccionaria: una meseta de 420–440 aristas en cuanto las piezas deben ser enteras, un muro PLE ya en el 8×8, y un récord académico de 461 en una hora. Lo que enseña el camino del optimizador, y dónde el LP sigue ganándose su lugar.
El ataque de los físicos a la satisfacción de restricciones: dividir el puzzle en dos conjuntos de restricciones cada uno fácil de proyectar, y luego iterar una aplicación cuyos puntos fijos son las soluciones. El método de Veit Elser llegó a la portada de PNAS y, sin embargo, en la lista de Eternity II sigue siendo un camino admirado, probado una vez y nunca recorrido hasta el final.