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

Technische Samenvatting: Noord–Oost Roosterpaden die $k$ Collineaire Punten Vermijden via Satisfiability

Probleemdefinitie
Dit artikel onderzoekt het Gerver–Ramsey collineariteitsprobleem, dat tracht de maximale lengte te bepalen van een noord–oost roosterpad (stappen in $\{(1,0), (0,1)\}$) dat het bevatten van $k$ collineaire punten vermijdt. Laat $a(k)$ de kleinste integer zijn waarvoor elk noord–oost roosterpad van lengte $a(k)$ $k$ collineaire punten bevat; bij consequentie is $a(k)-1$ de lengte van het langste dergelijke pad dat $k$ collineaire punten vermijdt. Hoewel Montgomery (1972) bewees dat een dergelijke grens voor alle $k$ bestaat, en Gerver en Ramsey (1979) een expliciete maar extreem ruime bovengrens boden, bleven de exacte waarden van $a(k)$ voor kleine $k$ grotendeels onbekend of computationeel moeilijk te verifiëren. Voorafgaand aan dit werk had J. Shallit (2013) computationeel bepaald dat $a(4)=9$, $a(5)=29$, en $a(6)=97$, en stelde een ondergrens vast van $a(7) \ge 261$ door een pad van lengte 260 te vinden.

Methodologie
De auteurs maken gebruik van Boolean Satisfiability (SAT) solving om deze roosterpaden te enumereren en te verifiëren. De kernaanpak bestaat uit het coderen van het bestaan van een pad van lengte $m$ dat $k$ collineaire punten vermijdt als een Conjunctive Normal Form (CNF) formule.

1. SAT Encoding:

   • Variabelen: Boolean variabelen $v_{x,y}$ representeren of punt $(x,y)$ op het pad ligt.
   • Pad-restricties: Clausules zorgen ervoor dat het pad begint bij $(0,0)$, alleen naar het Noorden of Oosten beweegt, en niet splitst (d.w.z. vanaf elk punt gaat het pad door naar precies één van de twee mogelijke volgende punten).
   • Niet-collineariteit restricties: De auteurs gebruiken cardinaliteitsrestricties (at-most-$k$) om te garanderen dat geen enkele lijn $k$ punten bevat. Deze worden naar CNF gecodeerd met behulp van sequential counter encodings of worden inheems afgehandeld via "at-least-$k$ conjunctive normal form" (KNF) met behulp van klauses.
   • Optimalisaties:
     • Symmetriebreking: De zoekruimte wordt verkleind door de eerste stap naar het Noorden af te dwingen, wat complementatie-symmetrie elimineert. Reversie-symmetrieën werden tijdens de zoektocht grotendeels genegeerd om encoding-overhead te vermijden, waarbij isomorfisme-checks post-enumeratie werden uitgevoerd.
     • Bereikbaarheidsgrenzen: Punten die bewezen onbereikbaar zijn (bijv. die $k-1$ opeenvolgende stappen in één richting vereisen) worden geblokkeerd via unit clauses.
     • Heuristiek voor het verwijderen van restricties: Om de efficiëntie van de solver te verbeteren, worden niet-collineariteit restricties die overeenkomen met lijnen met zeer weinig punten in het relevante gebied verwijderd. Als een oplossing wordt gevonden, wordt deze expliciet geverifieerd om te verzekeren dat er geen $k$ collineaire punten bestaan.
     • Parallellisatie: Voor grote instanties wordt de "cube-and-conquer" techniek gebruikt. Een lookahead solver (march) partitioneert de zoekruimte in disjuncte subproblemen (cubes), die vervolgens parallel kunnen worden opgelost.

2. Solver Selectie:

   • De auteurs benchmarkten standaard CNF encodings (opgelost door CaDiCaL) tegen KNF encodings (opgelost door Cardinality-CaDiCaL).
   • Resultaten gaven aan dat KNF significant beter presteert op bevredigbare instanties (het vinden van lange paden), terwijl CNF superieur is voor onbevredigbare instanties (het bewijzen van het niet-bestaan van langere paden). De methodologie past het type encoding aan op basis van of het doel het vinden van een pad of het bewijzen van de niet-existentie ervan is.

Belangrijkste Resultaten
Het artikel presenteert de volgende computationele resultaten:

• Enumeratie voor $k \le 6$: De auteurs hebben alle maximale GR($k$) walks (paden van lengte $a(k)-1$) tot isomorfisme geënumereerd voor $k \le 6$.

  • Bevestigde eerdere resultaten: $a(4)=9$, $a(5)=29$, en $a(6)=97$.
  • Vond dat er twee verschillende maximale GR(4) walks zijn, één unieke maximale GR(5) walk, en twee verschillende maximale GR(6) walks.
  • Genereerde DRAT proof certificates voor de niet-existentie van langere paden, wat onafhankelijke verificatie van de resultaten mogelijk maakt zonder de SAT-solver zelf te hoeven vertrouwen.

• Vooruitgang voor $k = 7$:

  • Verbetering Ondergrens: De auteurs ontdekten een GR(7) walk van lengte 327 stappen, wat de voorheen bekende beste lengte van 260 stappen van Shallit aanzienlijk verbetert.
  • Bereikbaarheidsanalyse: Ze bepaalden bovenste en onderste bereikbaarheidsgrenzen voor GR(7) walks tot 267 stappen en identificeerden het eerste onbereikbare punt op de lijn $y=x+1$ bij $(146, 147)$.
  • Zoekstrategie: De langste walks werden gevonden met een hybride aanpak bestaande uit random seed parallelisatie en cube-and-conquer. Opvallend genoeg waren de langste gevonden walks geconcentreerd nabij de lijn $y=x+1$.

Betekenis en Claims
Het artikel claimt dat SAT-solvers niet alleen effectief zijn voor het oplossen van discrete geometrische problemen met enorme zoekruimtes, maar ook een hoger niveau van betrouwbaarheid kunnen bieden dan op maat gemaakte zoekcode dankzij de mogelijkheid om bewijs-certificaten (DRAT-formaat) te genereren en te verifiëren.

De primaire bijdragen zijn:

1. Een SAT-gebaseerde methode voor het vinden van lange GR($k$) walks en het bewijzen van hun maximaliteit.
2. De volledige enumeratie van maximale GR($k$) walks voor $k \le 6$, waarmee eerdere computationele resultaten worden bevestigd en uitgebreid.
3. Een nieuwe ondergrens voor $a(7)$, waarbij de bekende langste pad van 260 naar 327 stappen is uitgebreid.
4. Een experimentele studie die aantoont dat, hoewel de exacte waarde van $a(7)$ nog steeds onbekend is, SAT-solving effectief de zoekruimte kan navigeren om aanzienlijk langere paden te vinden dan voorheen ontdekt, en dat bewijs-certificaten kunnen worden gegenereerd voor claims van niet-existentie.

De auteurs blijven bescheiden over de bepaling van $a(7)$ en merken op dat de exacte waarde nog steeds onbekend is, maar zij hopen dat hun introductie van SAT-solving voor dit probleem verdere vooruitgang zal faciliteren.