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

Sintesi Tecnica: Percorsi su Reticolo Nord-Est che Evitano $k$ Punti Collineari tramite la Soddisfacibilità

Definizione del Problema
Questo articolo investiga il problema della collinearità di Gerver–Ramsey, che mira a determinare la lunghezza massima di un percorso su reticolo nord-est (passaggi in $\{(1,0), (0,1)\}$) che eviti di contenere $k$ punti collineari. Sia $a(k)$ il più piccolo intero tale che ogni percorso su reticolo nord-est di lunghezza $a(k)$ contenga $k$ punti collineari; di conseguenza, $a(k)-1$ è la lunghezza del percorso più lungo che evita $k$ punti collineari. Sebbene Montgomery (1972) abbia dimostrato che un tale limite esiste per ogni $k$, e Gerver e Ramsey (1979) abbiano fornito un limite superiore esplicito ma estremamente debole, i valori esatti di $a(k)$ per piccoli $k$ sono rimasti in gran parte sconosciuti o computazionalmente difficili da verificare. Prima di questo lavoro, J. Shallit (2013) aveva determinato computazionalmente $a(4)=9$, $a(5)=29$ e $a(6)=97$, ed aveva stabilito un limite inferiore di $a(7) \ge 261$ trovando un percorso di lunghezza 260.

Metodologia
Gli autori utilizzano la risoluzione della Soddisfacibilità Booleana (SAT) per enumerare e verificare questi percorsi su reticolo. L'approccio principale consiste nel codificare l'esistenza di un percorso di lunghezza $m$ che eviti $k$ punti collineari come una formula in Forma Normale Congiuntiva (CNF).

1. Codifica SAT:

   • Variabili: Variabili booleane $v_{x,y}$ rappresentano se il punto $(x,y)$ è sul percorso.
   • Vincoli del Percorso: Le clausole assicurano che il percorso parta da $(0,0)$, si muova solo verso Nord o Est, e non si biforchi (ovvero, da ogni punto, il percorso procede verso esattamente uno dei due possibili punti successivi).
   • Vincoli di Non-Collinearità: Gli autori utilizzano vincoli di cardinalità (at-most-$k$) per garantire che nessuna retta contenga $k$ punti. Questi sono codificati in CNF utilizzando codifiche di contatori sequenziali o gestiti nativamente tramite "at-least-$k$ conjunctive normal form" (KNF) usando klauses.
   • Ottimizzazioni:
     • Rottura della Simmetria: Lo spazio di ricerca è ridotto imponendo che il primo passo sia verso Nord, eliminando la simmetria di complementazione. Le simmetrie di inversione sono state ampiamente ignorate durante la ricerca per evitare l'overhead di codifica, con controlli di isomorfismo eseguiti post-enumerazione.
     • Limiti di Raggiungibilità: I punti provati come irraggiungibili (ad esempio, quelli che richiedono $k-1$ passi consecutivi in una direzione) sono bloccati tramite clausole unitarie.
     • Eurisitica di Rimozione dei Vincoli: Per migliorare l'efficienza del solver, i vincoli di non-collinearità corrispondenti a rette con pochissimi punti nella regione rilevante vengono rimossi. Se viene trovato un percorso, esso viene esplicitamente verificato per garantire che non esistano $k$ punti collineari.
     • Parallelizzazione: Per istanze di grandi dimensioni, viene utilizzata la tecnica "cube-and-conquer". Un solver di lookahead (march) partiziona lo spazio di ricerca in sottoproblemi disgiunti (cubi), che vengono poi risolti in parallelo.

2. Selezione del Solver:

   • Gli autori hanno confrontato le standard codifiche CNF (risolte da CaDiCaL) rispetto alle codifiche KNF (risolte da Cardinality-CaDiCaL).
   • I risultati hanno indicato che la KNF performa significativamente meglio sulle istanze soddisfacibili (trovando percorsi lunghi), mentre la CNF è superiore sulle istanze insoddisfacibili (provando la non esistenza di percorsi più lunghi). La metodologia adatta il tipo di codifica in base al fatto che l'obiettivo sia trovare un percorso o provarne la non esistenza.

Risultati Chiave
L'articolo presenta i seguenti risultati computazionali:

• Enumerazione per $k \le 6$: Gli autori hanno enumerato esaustivamente tutti i percorsi massimali GR($k$) (percorsi di lunghezza $a(k)-1$) fino all'isomorfismo per $k \le 6$.

  • Confermato i risultati precedenti: $a(4)=9$, $a(5)=29$ e $a(6)=97$.
  • Trovato che esistono due percorsi massimali GR(4) distinti, un unico percorso massimale GR(5) e due percorsi massimali GR(6) distinti.
  • Generato certificati di prova DRAT per la non esistenza di percorsi più lunghi, consentendo la verifica indipendente dei risultati senza dover fidarsi del solver SAT stesso.

• Progressi per $k = 7$:

  • Miglioramento del Limite Inferiore: Gli autori hanno scoperto un percorso GR(7) di lunghezza 327 passi, migliorando significativamente la precedente migliore lunghezza nota di 260 passi trovata da Shallit.
  • Analisi di Raggiungibilità: Hanno determinato i limiti di raggiungibilità superiore e inferiore per i percorsi GR(7) fino a 267 passi e hanno identificato il primo punto irraggiungibile sulla retta $y=x+1$ al punto $(146, 147)$.
  • Strategia di Ricerca: I percorsi più lunghi sono stati trovati utilizzando un approccio ibrido che coinvolge la parallelizzazione con seed casuali e il cube-and-conquer. Notevolmente, i percorsi più lunghi trovati erano concentrati vicino alla retta $y=x+1$.

Significato e Rivendicazioni
L'articolo sostiene che i solver SAT non sono solo efficaci per risolvere problemi di geometria discreta con enormi spazi di ricerca, ma possono anche fornire livelli di affidabilità superiori rispetto al codice di ricerca scritto su misura grazie alla capacità di generare e verificare certificati di prova (formato DRAT).

I principali contributi sono:

1. Un metodo basato su SAT per trovare lunghi percorsi GR($k$) e provarne la massimalità.
2. La completa enumerazione dei percorsi massimali GR($k$) per $k \le 6$, confermando ed estendendo i precedenti risultati computazionali.
3. Un nuovo limite inferiore per $a(7)$, estendendo la lunghezza del percorso più lungo noto da 260 a 327 passi.
4. Uno studio sperimentale che dimostra come, sebbene il valore esatto di $a(7)$ rimanga sconosciuto, la risoluzione SAT possa navigare efficacemente lo spazio di ricerca per trovare percorsi significativamente più lunghi di quelli precedentemente scoperti, e che i certificati di prova possono essere generati per le affermazioni di non esistenza.

Gli autori rimangono modesti riguardo alla determinazione di $a(7)$, notando che il valore esatto è ancora sconosciuto, ma sperano che la loro introduzione della risoluzione SAT in questo problema possa facilitare ulteriori progressi.