North-East Lattice Paths Avoiding $k$ Collinear Points via Satisfiability

Resumen Técnico: Caminos de Red Norte-Este que Evitan $k$ Puntos Colineales mediante Satisfacibilidad

Definición del Problema
Este artículo investiga el problema de la colinealidad de Gerver–Ramsey, el cual busca determinar la longitud máxima de un camino de red norte-este (pasos en $\{(1,0), (0,1)\}$) que evita contener $k$ puntos colineales. Sea $a(k)$ el menor entero tal que todo camino de red norte-este de longitud $a(k)$ contiene $k$ puntos colineales; consecuentemente, $a(k)-1$ es la longitud del camino más largo que evita $k$ puntos colineales. Si bien Montgomery (1972) demostró que tal cota existe para todo $k$, y Gerver y Ramsey (1979) proporcionaron una cota superior explícita pero extremadamente laxa, los valores exactos de $a(k)$ para $k$ pequeños permanecían en gran medida desconocidos o eran computacionalmente difíciles de verificar. Antes de este trabajo, J. Shallit (2013) había determinado computacionalmente que $a(4)=9$, $a(5)=29$ y $a(6)=97$, y estableció una cota inferior de $a(7) \ge 261$ mediante el hallazgo de un camino de longitud 260.

Metodología
Los autores emplean la resolución de Satisfacibilidad Booleana (SAT) para enumerar y verificar estos caminos de red. El enfoque central consiste en codificar la existencia de un camino de longitud $m$ que evita $k$ puntos colineales como una fórmula en Forma Normal Conjuntiva (CNF).

1. Codificación SAT:

   • Variables: Las variables booleanas $v_{x,y}$ representan si el punto $(x,y)$ está en el camino.
   • Restricciones del Camino: Las cláusulas aseguran que el camino comience en $(0,0)$, se mueva solo hacia el Norte o el Este, y no se bifurque (es decir, desde cualquier punto, el camino procede hacia exactamente uno de los dos posibles puntos siguientes).
   • Restricciones de No Colinealidad: Los autores utilizan restricciones de cardinalidad (at-most-$k$) para asegurar que ninguna línea contenga $k$ puntos. Esto se codifica en CNF utilizando codificaciones de contador secuencial o se maneja de forma nativa mediante una "forma normal conjuntiva de al menos $k$" (KNF) usando klauses.
   • Optimizaciones:
     • Ruptura de Simetría: Se reduce el espacio de búsqueda imponiendo que el primer paso sea al Norte, eliminando la simetría de complementación. Las simetrías de reversión fueron mayormente ignoradas durante la búsqueda para evitar la sobrecarga de codificación, realizando las comprobaciones de isomorfismo post-enumeración.
     • Límites de Alcance: Los puntos probados como inalcanzables (por ejemplo, aquellos que requieren $k-1$ pasos consecutivos en una sola dirección) son bloqueados mediante cláusulas unitarias.
     • Heurística de Eliminación de Restricciones: Para mejorar la eficiencia del solver, se eliminan las restricciones de no colinealidad correspondientes a líneas con muy pocos puntos en la región relevante. Si se encuentra una solución, esta se verifica explícitamente para asegurar que no existan $k$ puntos colineales.
     • Paralelización: Para instancias grandes, se utiliza la técnica "cube-and-conquer". Un solver de anticipación (lookahead solver o march) particiona el espacio de búsqueda en subproblemas disjuntos (cubos), que luego se resuelven en paralelo.

2. Selección del Solver:

   • Los autores compararon codificaciones CNF estándar (resueltas por CaDiCaL) frente a codificaciones KNF (resueltas por Cardinality-CaDiCaL).
   • Los resultados indicaron que KNF funciona significativamente mejor en instancias satisfactorias (hallando caminos largos), mientras que CNF es superior para instancias insatisfactorias (probando la no existencia de caminos más largos). La metodología adapta el tipo de codificación dependiendo de si el objetivo es encontrar un camino o probar su no existencia.

Resultados Clave
El artículo presenta los siguientes resultados computacionales:

• Enumeración para $k \le 6$: Los autores enumeraron exhaustivamente todos los caminos GR($k$) maximales (caminos de longitud $a(k)-1$) hasta el isomorfismo para $k \le 6$.

  • Confirmaron resultados previos: $a(4)=9$, $a(5)=29$ y $a(6)=97$.
  • Encontraron que existen dos caminos GR(4) maximales distintos, un único camino GR(5) maximal y dos caminos GR(6) maximales distintos.
  • Generaron certificados de prueba DRAT para la no existencia de caminos más largos, lo que permite la verificación independiente de los resultados sin confiar en el propio solver SAT.

• Avances para $k = 7$:

  • Mejora de la Cota Inferior: Los autores descubrieron un camino GR(7) de 327 pasos, mejorando significativamente la mejor longitud conocida de 260 pasos de Shallit.
  • Análisis de Alcance: Determinaron los límites de alcance superior e inferior para caminos GR(7) hasta los 267 pasos e identificaron el primer punto inalcanzable en la línea $y=x+1$ en $(146, 147)$.
  • Estrategia de Búsqueda: Los caminos más largos se encontraron utilizando un enfoque híbrido que involucra paralelización de semillas aleatorias y cube-and-conquer. Notablemente, los caminos más largos encontrados se concentraron cerca de la línea $y=x+1$.

Significancia y Reivindicaciones
El artículo sostiene que los solvers SAT no solo son efectivos para resolver problemas de geometría discreta con espacios de búsqueda enormes, sino que también pueden proporcionar niveles de confianza más altos que el código de búsqueda escrito a medida debido a la capacidad de generar y verificar certificados de prueba (formato DRAT).

Las principales contribuciones son:

1. Un método basado en SAT para encontrar caminos GR($k$) largos y probar su maximalidad.
2. La enumeración completa de los caminos GR($k$) maximales para $k \le 6$, confirmando y extendiendo resultados computacionales previos.
3. Una nueva cota inferior para $a(7)$, extendiendo la longitud de camino más larga conocida de 260 a 327 pasos.
4. Un estudio experimental que demuestra que, aunque el valor exacto de $a(7)$ sigue siendo desconocido, la resolución de SAT puede navegar eficazmente el espacio de búsqueda para encontrar caminos significativamente más largos que los descubiertos anteriormente, y que se pueden generar certificados de prueba para reclamaciones de no existencia.

Los autores mantienen la modestia respecto a la determinación de $a(7)$, señalando que el valor exacto aún es desconocido, pero esperan que su introducción de la resolución de SAT en este problema facilite progresos adicionales.