🔢 mathematics

Queen Domination by SAT Solving

Este artículo presenta un marco de SAT de alto rendimiento y con producción de pruebas que resuelve el caso previamente abierto de la dominación de reinas para $n=19$ y corrige la enumeración para $n=16$ mediante el aprovechamiento de una codificación informada geométricamente, la ruptura de simetrías y un proceso de verificación unificado para asegurar una corrección verificable de forma independiente.

Autores originales: Taha Rostami, Curtis Bright

Publicado 2026-07-30

📖 4 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Taha Rostami, Curtis Bright

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina un mundo donde las matemáticas no son solo números en una página, sino la resolución de acertijos tan complejos que incluso los cerebros humanos más inteligentes se marean. Este es el reino de la búsqueda combinatoria, una rama de la informática y las matemáticas dedicada a encontrar la mejor manera de organizar las cosas. Piensa en ello como intentar encontrar el plano de asientos perfecto para una boda masiva donde cada invitado tiene reglas específicas sobre con quién puede sentarse, o determinar el número absoluto mínimo de guardias de seguridad necesarios para vigilar cada rincón de un museo sin dejar un punto ciego.

Uno de los acertijos más famosos en este campo es el Problema de la Dominación de la Reina. Imagina un tablero de ajedrez. Una reina es una pieza poderosa que puede atacar todo en su fila, su columna y ambos caminos diagonales. La pregunta es simple pero complicada: ¿Cuál es el número mínimo de reinas que necesitas colocar en un tablero de $n \times n$ para que cada casilla esté bajo ataque? Parece fácil para un tablero pequeño, pero a medida que el tablero se agranda, el número de posibles arreglos explota hacia los miles de millones, billones y más allá. Durante más de un siglo, los matemáticos han intentado resolver esto, no solo para encontrar el número, sino para contar exactamente cuántas formas diferentes existen de disponer esas reinas. ¿Por qué importa esto? Porque resolver estos acertijos nos ayuda a entender cómo organizar sistemas complejos, desde la programación de vuelos hasta el diseño de chips de computadora. Pero hay un inconveniente: cuando las computadoras hacen las matemáticas, pueden cometer errores y, a veces, pasan por alto la respuesta por completo.

Aquí es donde intervienen Taha Rostami y Curtis Bright con su artículo, "Queen Domination by SAT Solving". Ellos abordaron el problema de contar todas las formas únicas de colocar el número mínimo de reinas en tableros de ajedrez de hasta tamaño 19. En lugar de escribir un programa personalizado para cazar soluciones como hicieron investigadores anteriores, tradujeron todo el acertijo del tablero de ajedrez a un lenguaje que un solucionador SAT (una máquina de lógica superinteligente) entiende. Piensa en un solucionador SAT como un detective que comprueba si un conjunto de reglas puede ser verdadero alguna vez. Si el detective dice "no", puede probarlo con un certificado que cualquier otra persona pueda verificar para asegurarse de que el detective no mintió.

Los autores construyeron una "traducción" especial del tablero de ajedrez que resaltaba la geometría del juego, utilizando un truco ingenioso llamado curva de Hilbert para organizar las pistas de modo que el detective pudiera encontrar la respuesta más rápido. También utilizaron una estrategia llamada Cube-and-Conquer, que es como dividir un pastel gigante e imposible de comer en miles de rebanadas pequeñas y manejables que diferentes computadoras puedan comer al mismo tiempo. ¿El resultado? No solo resolvieron el acertijo; demostraron que su solución era 100% correcta.

Su trabajo descubrió un error sorprendente en la historia de este problema. Para un tablero de 16x16, expertos previos pensaban que solo había 43 formas únicas de colocar las reinas. Rostami y Bright demostraron que en realidad hay 371 formas, una diferencia masiva que sugiere que el antiguo programa de computadora tenía un error oculto que estaba perdiendo la mayoría de las soluciones. Además, resolvieron un caso que había estado abierto durante mucho tiempo: el tablero de 19x19. Encontraron que hay exactamente 11 formas únicas de dominar ese tablero con el número mínimo de reinas. Al generar "certificados de prueba" para cada uno de los resultados, le dieron a la comunidad matemática un nivel de confianza que antes era imposible, demostrando que cuando se combina una codificación inteligente con una verificación de pruebas rigurosa, se pueden resolver problemas que incluso el mejor software especializado podría pasar por alto.

Resumen Técnico: Dominación de Reinas mediante la Resolución de SAT

Definición del Problema
El problema de la dominación de reinas busca el número mínimo de reinas, denotado como $\gamma(Q_n)$ , necesarias para atacar cada casilla en un tablero de ajedrez de $n \times n$ . Más allá de determinar este valor mínimo, un desafío significativo radica en enumerar todas las soluciones distintas hasta el isomorfismo (considerando las simetrías del tablero como rotación y reflexión). Si bien los valores óptimos para $\gamma(Q_n)$ han sido establecidos para $n \le 25$ utilizando herramientas de búsqueda especializadas como UNIDOM, la enumeración de soluciones no isomórficas para tableros más grandes sigue siendo computacionalmente intensiva. Una preocupación crítica en este dominio es la fiabilidad de los resultados computacionales; las discrepancias previas en otros problemas combinatorios (por ejemplo, el problema de Lam) y el descubrimiento de errores en solvers especializados resaltan la necesidad de certificados de corrección verificables de forma independiente.

Metodología
Los autores proponen un marco de Satisfacibilidad Booleana (SAT) productor de pruebas para abordar el problema de la dominación de reinas. En lugar de implementar un algoritmo de búsqueda personalizado, el problema se codifica en una fórmula proposicional en Forma Normal Conjuntiva (CNF). La metodología se basa en varias innovaciones técnicas clave:

Codificación de Variables de Línea: La innovación central es la introducción de variables booleanas auxiliares que representan si líneas geométricas específicas (filas, columnas, diagonales y antidiagonales) contienen al menos una reina.
- Variables de Reina ( $Q_i$ ): Indican si una reina está colocada en la casilla $i$ .
- Variables de Línea ( $L_\ell$ ): Indican si una línea $\ell$ está "activa" (contiene una reina).
- Restricciones: Las cláusulas aseguran que, si una línea está activa, existe una reina en ella. La dominación se expresa requiriendo que, para cada casilla, al menos una de sus cuatro líneas que la intersectan esté activa. Las restricciones de cardinalidad limitan el número total de reinas ( $\sum Q_i \le \gamma$ ) y el número total de líneas activas ( $\sum L_\ell \le 4\gamma$ ).
Codificación de Cardinalidad y Ordenamiento de Literales:
- Las restricciones de cardinalidad se codifican utilizando métodos basados en totalizers. La restricción de reinas utiliza un totalizer estándar compatible con el marco Cube-and-Conquer, mientras que la restricción de líneas utiliza un modulo totalizer para mejorar el rendimiento.
- Ordenamiento de Curva de Hilbert: Se aplica una novedosa estrategia de ordenamiento de literales a la restricción de cardinalidad de las reinas. Al recorrer el tablero mediante una curva de Hilbert, las casillas espacialmente adyacentes se agrupan en el árbol de conteo. Esto preserva la localidad espacial, lo que conduce a una propagación de unidad más fuerte. Los experimentos mostraron que este ordenamiento resolvió la instancia de $n=14$ aproximadamente 31.5 veces más rápido que el ordenamiento por defecto.
Ruptura de Simetría: Para eliminar la exploración redundante de soluciones simétricas, el marco impone restricciones de orden lexicográfico (basadas en el método de Warwick Harvey) entre la configuración original de las reinas y sus siete transformaciones geométricas de no identidad. Esto redujo significamente los tiempos de resolución en pruebas preliminares (por ejemplo, una aceleración de 6.64× para $n=15$ ).
Cube-and-Conquer: Para instancias más grandes, el espacio de búsqueda se particiona en subproblemas independientes (cubos) mediante la ramificación en variables auxiliares del encoding del totalizer. Esto permite la resolución en paralelo y mejora la escalabilidad sin depender de las colocaciones individuales de las reinas para la partición.
Generación de Pruebas y Verificación: El marco utiliza cadical-exhaust para enumerar todos los modelos mediante la adición iterativa de cláusulas de bloqueo. Genera pruebas DRAT con "cláusulas de confianza" para certificar la completitud. Estas pruebas se verifican de forma independiente utilizando drat-trim-t, asegurando que los resultados no dependan de la corrección interna de la lógica de búsqueda del solver, sino únicamente del encoding y del verificador de pruebas.

Resultados Clave
El estudio logró enumerar con éxito las soluciones no isomórficas mínimas de dominación de reinas para todo $n \le 19$ . Los resultados incluyen:

Corrección de la Literatura: Para $n=16$ , el artículo identifica una discrepancia en informes previos. Mientras que el solver especializado UNIDOM reportó 43 soluciones no isomórficas, el marco SAT demuestra que hay exactamente 371. Los autores atribuyen esto a un error en UNIDOM que causa que se omitan soluciones válidas bajo configuraciones específicas.
Resolución de Caso Abierto: El caso previamente abierto de $n=19$ se resuelve, estableciendo que existen exactamente 11 soluciones mínimas no isomórficas.
Rendimiento: El marco SAT superó consistentemente al solver especializado UNIDOM en instancias no triviales. Para $n=19$ , el enfoque SAT tomó aproximadamente 171,575 segundos (tiempo de CPU) para la enumeración, comparado con los 714,733 segundos de UNIDOM. La inclusión de las variables de línea fue crucial; una versión preliminar sin ellas tardó 22.8 veces más en resolver y verificar la instancia de $n=19$ .

Significancia y Reivindicaciones
El artículo afirma que su contribución principal es proporcionar una solución de alto rendimiento e independientemente verificable al problema de la enumeración de la dominación de reinas. Al cambiar de un código de búsqueda especializado a un marco SAT productor de pruebas, los autores reducen la "confianza" requerida en el proceso computacional. La corrección de los resultados depende únicamente del encoding de SAT y del verificador de pruebas externo, en lugar de la compleja lógica personalizada de un solver especializado.

Este trabajo demuestra que un diseño de codificación cuidadoso —específicamente la introducción de variables auxiliares para exponer la estructura geométrica, el uso de restricciones globales y el ordenamiento de literales consciente de la geometría— puede hacer que la resolución de SAT productora de pruebas sea competitiva con, y superior a, los solvers altamente optimizados de dominio específico. Los autores ponen su código fuente y datos de solución a disposición pública para facilitar una mayor verificación e investigación.

Más como este