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

Résumé Technique : Chemins de réseaux Nord-Est évitant $k$ points colinéaires via la satisfaction de contraintes (SAT)

Définition du Problème
Cet article étudie le problème de colinéarité de Gerver–Ramsey, qui cherche à déterminer la longueur maximale d'un chemin de réseau nord-est (étapes dans $\{(1,0), (0,1)\}$) qui évite de contenir $k$ points colinéaires. Soit $a(k)$ le plus petit entier tel que tout chemin de réseau nord-est de longueur $a(k)$ contient $k$ points colinéaires ; par conséquent, $a(k)-1$ est la longueur du plus long chemin de ce type évitant $k$ points colinéaires. Bien que Montgomery (1972) ait prouvé qu'une telle borne existe pour tout $k$, et que Gerver et Ramsey (1979) aient fourni une borne supérieure explicite mais extrêmement lâche, les valeurs exactes de $a(k)$ pour de petits $k$ restaient largement inconnues ou difficiles à vérifier par calcul. Avant ce travail, J. Shallit (2013) avait déterminé par calcul $a(4)=9$, $a(5)=29$ et $a(6)=97$, et avait établi une borne inférieure de $a(7) \ge 261$ en trouvant un chemin de longueur 260.

Méthodologie
Les auteurs utilisent la résolution de problèmes de satisfaction de contraintes booléennes (SAT) pour énumérer et vérifier ces chemins de réseau. L'approche centrale consiste à encoder l'existence d'un chemin de longueur $m$ évitant $k$ points colinéaires sous la forme d'une formule de Forme Normale Conjonctive (CNF).

1. Encodage SAT :

   • Variables : Les variables booléennes $v_{x,y}$ représentent si le point $(x,y)$ est sur le chemin.
   • Contraintes de chemin : Les clauses garantissent que le chemin commence à $(0,0)$, ne se déplace que vers le Nord ou l'Est, et ne se divise pas (c'est-à-dire que depuis n'importe quel point, le chemin progresse vers exactement un des deux points suivants possibles).
   • Contraintes de non-colinéarité : Les auteurs utilisent des contraintes de cardinalité (au plus-$k$) pour garantir qu'aucune droite ne contient $k$ points. Celles-ci sont encodées en CNF via des encodages de compteurs séquentiels ou gérées nativement via des formes normales conjonctives (KNF) utilisant des « klauses ».
   • Optimisations :
     • Rupture de Symétrie : L'espace de recherche est réduit en imposant que le premier pas soit vers le Nord, éliminant ainsi la symétrie de complémentarité. Les symétries de renversement ont été largement ignorées pendant la recherche pour éviter la surcharge d'encodage, les vérifications d'isomorphisme étant effectuées après l'énumération.
     • Bornes de l'accessibilité : Les points prouvés inaccessibles (par exemple, ceux nécessitant $k-1$ étapes consécutives dans une même direction) sont bloqués via des clauses unitaires.
     • Heuristique de suppression de contrainte : Pour améliorer l'efficacité du solveur, les contraintes de non-colinéarité correspondant à des droites possédant très peu de points dans la région concernée sont supprimées. Si une solution est trouvée, elle est explicitement vérifiée pour s'assurer qu'il n'existe pas $k$ points colinéaires.
     • Parallélisation : Pour les instances de grande taille, la technique « cube-and-conquer » est utilisée. Un solveur d'anticipation (lookahead solver ou march) partitionne l'espace de recherche en sous-problèmes disjoints (« cubes »), qui sont ensuite résolus en parallèle.

2. Sélection du Solveur :

   • Les auteurs ont comparé des encodages CNF standards (résolus par CaDiCaL) par rapport aux encodages KNF (résolus par Cardinality-CaDiCaL).
   • Les résultats ont indiqué que la KNF est nettement plus performante sur les instances satisfaisables (trouvant des chemins longs), tandis que la CNF est supérieure pour les instances insatisfaisables (prouvant la non-existence de chemins plus longs). La méthodologie adapte le type d'encodage en fonction de l'objectif : trouver un chemin ou prouver sa non-existence.

Résultats Clés
Le papier présente les résultats computationnels suivants :

• Énumération pour $k \le 6$ : Les auteurs ont énuméré de manière exhaustive tous les chemins maximaux GR($k$) (chemins de longueur $a(k)-1$) à isomorphisme près pour $k \le 6$.

  • Confirmation des résultats précédents : $a(4)=9$, $a(5)=29$ et $a(6)=97$.
  • Ont trouvé qu'il existe deux marches GR(4) distinctes et maximales, une marche GR(5) unique et maximale, et deux marches GR(6) distinctes et maximales.
  • Génération de certificats de preuve DRAT pour la non-existence de chemins plus longs, permettant une vérification indépendante des résultats sans dépendre de la fiabilité du solveur SAT lui-même.

• Avancées pour $k = 7$ :

  • Amélioration de la Borne Inférieure : Les auteurs ont découvert une marche GR(7) de longueur 327 étapes, améliorant significativement la meilleure longueur connue de 260 étapes établie par Shallit.
  • Analyse d'Accessibilité : Ils ont déterminé les bornes d'accessibilité supérieure et inférieure pour les marches GR(7) jusqu'à 267 étapes et ont identifié le premier point inaccessible sur la droite $y=x+1$ à $(146, 147)$.
  • Stratégie de Recherche : Les marches les plus longues ont été trouvées grâce à une approche hybride impliquant une parallélisation par graines aléatoires (random seed parallelization) et le « cube-and-conquer ». Notamment, les marches les plus longues trouvées étaient concentrées près de la droite $y=x+1$.

Signification et Revendications
Le papier affirme que les solveurs SAT ne sont pas seulement efficaces pour résoudre des problèmes de géométrie discrète avec des espaces de recherche énormes, mais qu'ils peuvent également offrir un niveau de confiance supérieur au code de recherche personnalisé grâce à la capacité de générer et de vérifier des certificats de preuve (format DRAT).

Les principales contributions sont :

1. Une méthode basée sur le SAT pour trouver de longues marches GR($k$) et prouver leur maximalité.
2. L'énumération complète des marches GR($k$) maximales pour $k \le 6$, confirmant et étendant les résultats computationnels précédents.
3. Une nouvelle borne inférieure pour $a(7)$, portant la longueur du chemin le plus long connu de 260 à 327 étapes.
4. Une étude expérimentale démontrant que, bien que la valeur exacte de $a(7)$ reste inconnue, la résolution par SAT peut naviguer efficacement dans l'espace de recherche pour trouver des chemins nettement plus longs que ceux découverts précédemment, et que des certificats de preuve peuvent être générés pour les affirmations de non-existence.

Les auteurs restent modestes quant à la détermination de $a(7)$, notant que sa valeur exacte est toujours inconnue, mais espèrent que l'introduction de la résolution par SAT à ce problème facilitera les progrès futurs.