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

Technisches Resümee: Nord-Ost-Gitterpfade, die $k$ kollineare Punkte vermeiden, mittels Erfüllbarkeitsproblemen

Problemdefinition
Diese Arbeit untersucht das Gerver–Ramsey-Kollinearitätsproblem, welches die Bestimmung der maximalen Länge eines Nord-Ost-Gitterpfades (Schritte in $\{(1,0), (0,1)\}$) sucht, der keine $k$ kollinearen Punkte enthält. Sei $a(k)$ die kleinste Ganzzahl, sodass jeder Nord-Ost-Gitterpfad der Länge $a(k)$ genau $k$ kollineare Punkte enthält; folglich ist $a(k)-1$ die Länge des längsten solchen Pfades, der $k$ kollineare Punkte vermeidet. Während Montgomery (1972) bewies, dass eine solche Schranke für alle $k$ existiert, und Gerver sowie Ramsey (1979) eine explizite, aber extrem lose obere Schranke lieferten, blieben die exakten Werte von $a(k)$ für kleine $k$ weitgehend unbekannt oder waren computational schwierig zu verifizieren. Vor dieser Arbeit hatte J. Shallit (2013) computergestützt $a(4)=9$, $a(5)=29$ und $a(6)=97$ ermittelt und eine untere Schranke von $a(7) \ge 261$ durch das Finden eines Pfades der Länge 260 etabliert.

Methodik
Die Autoren setzen SAT-Solver (Boolean Satisfiability) ein, um diese Gitterpfade zu enumerieren und zu verifizieren. Der Kernansatz besteht darin, die Existenz eines Pfades der Länge $m$, der $k$ kollineare Punkte vermeidet, als eine Konjunktive Normalform (CNF)-Formel zu kodieren.

1. SAT-Kodierung:

   • Variablen: Boolesche Variablen $v_{x,y}$ repräsentieren, ob der Punkt $(x,y)$ auf dem Pfad liegt.
   • Pfad-Constraints: Klauseln stellen sicher, dass der Pfad bei $(0,0)$ beginnt, sich nur nach Norden oder Osten bewegt und sich nicht aufspaltet (d. h. von jedem Punkt aus führt der Pfad zu genau einem der zwei möglichen nächsten Punkte).
   • Nicht-Kollinearitäts-Constraints: Die Autoren verwenden Kardinalitätsbeschränkungen (At-most-$k$), um sicherzustellen, dass keine Gerade $k$ Punkte enthält. Diese werden mittels sequenzieller Zähler-Kodierungen in CNF kodiert oder nativ über „At-least-$k$ konjunktive Normalform“ (KNF) mittels Klauseln gehandhabt.
   • Optimierungen:
     • Symmetriebrechung: Der Suchraum wird reduziert, indem der erste Schritt als Nord erzwungen wird, was die Komplementationssymmetrie eliminiert. Reversionssymmetrien wurden während der Suche weitgehend ignoriert, um den Kodierungsaufwand zu vermeiden, wobei Isomorphie-Prüfungen nach der Enumeration durchgeführt wurden.
     • Erreichbarkeits-Schranken: Punkte, die nachweislich unerreichbar sind (z. B. solche, die $k-1$ aufeinanderfolgende Schritte in eine Richtung erfordern), werden durch Unit-Klauseln blockiert.
     • Heuristik zur Entfernung von Constraints: Um die Effizienz des Solvers zu verbessern, werden Nicht-Kollinearitäts-Constraints, die zu Linien mit sehr wenigen Punkten im relevanten Bereich gehören, entfernt. Wenn eine Lösung gefunden wird, wird diese explizit verifiziert, um sicherzustellen, dass keine $k$ kollinearen Punkte existieren.
     • Parallelisierung: Für große Instanzen wird die „Cube-and-Conquer“-Technik angewendet. Ein Lookahead-Solver (March) partitioniert den Suchraum in disjunkte Teilprobleme (Cubes), die dann parallel gelöst werden.

2. Solver-Auswahl:

   • Die Autoren benchmarkten Standard-CNF-Kodierungen (gelöst durch CaDiCaL) gegen KNF-Kodierungen (gelöst durch Cardinality-CaDiCaL).
   • Die Ergebnisse zeigten, dass KNF bei erfüllbaren Instanzen (Finden langer Pfade) signifikant besser abschneidet, während CNF bei unerfüllbaren Instanzen (Beweis der Nichtexistenz längerer Pfade) überlegen ist. Die Methodik passt den Kodierungstyp an, je nachdem, ob das Ziel darin besteht, einen Pfad zu finden oder dessen Nichtexistenz zu beweisen.

Wesentliche Ergebnisse
Das Paper präsentiert die folgenden computergestützten Ergebnisse:

• Enumeration für $k \le 6$: Die Autoren haben alle maximalen GR($k$)-Walks (Pfade der Länge $a(k)-1$) bis zur Isomorphie für $k \le 6$ vollständig enumeriert.

  • Bestätigte frühere Ergebnisse: $a(4)=9$, $a(5)=29$ und $a(6)=97$.
  • Es wurde festgestellt, dass es zwei distinkte maximale GR(4)-Walks gibt, einen eindeutigen maximalen GR(5)-Walk und zwei distinkte maximale GR(6)-Walks.
  • Es wurden DRAT-Beweiszertifikate generiert, um die Nichtexistenz längerer Pfade zu belegen, was eine unabhängige Verifizierung der Ergebnisse ermöglicht, ohne dem SAT-Solver selbst vertrauen zu müssen.

• Fortschritte für $k = 7$:

  • Verbesserung der unteren Schranke: Die Autoren entdeckten einen GR(7)-Walk der Länge 327 Schritte, was die bisher beste bekannte Länge von 260 Schritten (gefunden von Shallit) signifikant verbessert.
  • Erreichbarkeitsanalyse: Sie bestimmten obere und untere Erreichbarkeitsgrenzen für GR(7)-Walks bis zu einer Länge von 267 Schritten und identifizierten den ersten unerreichbaren Punkt auf der Linie $y=x+1$ bei $(146, 147)$.
  • Suchstrategie: Die längsten Walks wurden mittels eines hybriden Ansatzes gefunden, der Random-Seed-Parallelisierung und Cube-and-Conquer kombiniert. Bemerkenswerterweise waren die längsten gefundenen Walks in der Nähe der Linie $y=x+1$ konzentriert.

Bedeutung und Behauptungen
Das Paper behauptet, dass SAT-Solver nicht nur effektiv für die Lösung diskreter Geometrieprobleme mit enormen Suchräumen sind, sondern auch ein höheres Maß an Vertrauenswürdigkeit bieten können als eigens geschriebener Suchcode, da sie Beweis-Zertifikate (DRAT-Format) generieren und verifizieren können.

Die primären Beiträge sind:

1. Eine SAT-basierte Methode zum Finden langer GR($k$)-Walks und zum Beweis ihrer Maximalität.
2. Die vollständige Enumeration maximaler GR($k$)-Walks für $k \le 6$, welche frühere computergestützte Ergebnisse bestätigt und erweitert.
3. Eine neue untere Schranke für $a(7)$, welche die bisher bekannte längste Pfadlänge von 260 auf 327 Schritte erweitert.
4. Eine experimentelle Studie, die zeigt, dass SAT-Solving, obwohl der exakte Wert von $a(7)$ weiterhin unbekannt bleibt, effektiv durch den Suchraum navigieren kann, um signifikant längere Pfade als zuvor entdeckt zu finden, und dass Beweis-Zertifikate für Nichtexistenz-Behauptungen generiert werden können.

Die Autoren bleiben bescheiden hinsichtlich der Bestimmung von $a(7)$ und merken an, dass der exakte Wert weiterhin unbekannt ist, hoffen jedoch, dass ihre Einführung des SAT-Solving für dieses Problem weitere Fortschritte ermöglichen wird.