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

Resumo Técnico: Caminhos de Rede Norte-Nordeste Evitando $k$ Pontos Colineares via Satisfatibilidade

Definição do Problema
Este artigo investiga o problema da colinearidade de Gerver–Ramsey, que busca determinar o comprimento máximo de um caminho de rede norte-nordeste (passos em $\{(1,0), (0,1)\}$) que evita conter $k$ pontos colineares. Seja $a(k)$ o menor inteiro tal que todo caminho de rede norte-nordeste de comprimento $a(k)$ contém $k$ pontos colineares; consequentemente, $a(k)-1$ é o comprimento do caminho mais longo que evita $k$ pontos colineares. Embora Montgomery (1972) tenha provado que tal limite existe para todo $k$, e Gerver e Ramsey (1979) tenham fornecido um limite superior explícito, porém extremamente frouxo, os valores exatos de $a(k)$ para pequenos $k$ permaneciam amplamente desconhecidos ou computacionalmente difíceis de verificar. Antes deste trabalho, J. Shallit (2013) determinou computacionalmente $a(4)=9$, $a(5)=29$ e $a(6)=97$, e estabeleceu um limite inferior de $a(7) \ge 261$ ao encontrar um caminho de comprimento 260.

Metodologia
Os autores empregam a resolução de Satisfatibilidade Booleana (SAT) para enumerar e verificar esses caminhos de rede. A abordagem central envolve codificar a existência de um caminho de comprimento $m$ que evita $k$ pontos colineares como uma fórmula de Forma Normal Conjuntiva (CNF).

1. Codificação SAT:

   • Variáveis: Variáveis booleanas $v_{x,y}$ representam se o ponto $(x,y)$ está no caminho.
   • Restrições de Caminho: Cláusulas garantem que o caminho comece em $(0,0)$, mova-se apenas para o Norte ou para o Leste, e não se divida (ou seja, de qualquer ponto, o caminho procede para exatamente um dos dois próximos pontos possíveis).
   • Restrições de Não-Colinearidade: Os autores utilizam restrições de cardinalidade (no-máximo-$k$) para garantir que nenhuma linha contenha $k$ pontos. Estas são codificadas em CNF usando codificações de contador sequencial ou tratadas nativamente via "forma normal conjuntiva de pelo-menos-$k$" (KNF) usando klauses.
   • Otimizações:
     • Quebra de Simetria: O espaço de busca é reduzido ao impor que o primeiro passo seja para o Norte, eliminando a simetria de complementação. Simetrias de reversão foram amplamente ignoradas durante a busca para evitar sobrecarga de codificação, com verificações de isomorfismo realizadas pós-enumeração.
     • Limites de Alcance: Pontos provados como inalcançáveis (por exemplo, aqueles que exigem $k-1$ passos consecutivos em uma única direção) são bloqueados via cláusulas unitárias.
     • Heurística de Remoção de Restrição: Para melhorar a eficiência do solver, restrições de não-colinearidade correspondentes a linhas com poucos pontos na região relevante são removidas. Se uma solução é encontrada, ela é explicitamente verificada para garantir que não existam $k$ pontos colineares.
     • Paralelização: Para instâncias grandes, a técnica "cube-and-conquer" é utilizada. Um solver de lookahead (march) particiona o espaço de busca em subproblemas disjuntos (cubes), que são então resolvidos em paralelo.

2. Seleção de Solver:

   • Os autores compararam codificações CNF padrão (resolvidas por CaDiCaL) contra codificações KNF (resolvidas por Cardinality-CaDiCaL).
   • Os resultados indicaram que o KNF performa significativamente melhor em instâncias satisfatíveis (encontrando caminhos longos), enquanto o CNF é superior em instâncias insatisfatíveis (provando a não existência de caminhos mais longos). A metodologia adapta o tipo de codificação com base se o objetivo é encontrar um caminho ou provar sua não existência.

Principais Resultados
O artigo apresenta os seguintes resultados computacionais:

• Enumeração para $k \le 6$: Os autores enumeraram exaustivamente todos os caminhos GR($k$) maximais (caminhos de comprimento $a(k)-1$) até o isomorfismo para $k \le 6$.

  • Confirmou resultados anteriores: $a(4)=9$, $a(5)=29$ e $a(6)=97$.
  • Descobriu que existem dois caminhos GR(4) maximais distintos, um único caminho GR(5) maximal e dois caminhos GR(6) maximais distintos.
  • Gerou certificados de prova DRAT para a não existência de caminhos mais longos, permitindo a verificação independente dos resultados sem confiar no próprio solver SAT.

• Avanços para $k = 7$:

  • Melhoria do Limite Inferior: Os autores descobriram um caminho GR(7) de comprimento 327 passos, melhorando significativamente o comprimento anterior de 260 passos encontrado por Shallit.
  • Análise de Alcance: Eles determinaram limites de alcance superior e inferior para caminhos GR(7) até 267 passos e identificaram o primeiro ponto inalcançável na linha $y=x+1$ em $(146, 147)$.
  • Estratégia de Busca: Os caminhos mais longos foram encontrados usando uma abordagem híbrida envolvendo paralelização de sementes aleatórias e cube-and-conquer. Notavelmente, os caminhos mais longos encontrados concentravam-se próximo à linha $y=x+1$.

Significância e Alegações
O artigo alega que os solvers SAT não são apenas eficazes para resolver problemas de geometria discreta com espaços de busca enormes, mas também podem fornecer níveis de confiança superiores a códigos de busca escritos sob medida devido à capacidade de gerar e verificar certificados de prova (formato DRAT).

As principais contribuições são:

1. Um método baseado em SAT para encontrar longos caminhos GR($k$) e provar sua maximalidade.
2. A enumeração completa de caminhos GR($k$) maximais para $k \le 6$, confirmando e estendendo resultados computacionais anteriores.
3. Um novo limite inferior para $a(7)$, estendendo o caminho mais longo conhecido de 260 para 327 passos.
4. Um estudo experimental demonstrando que, embora o valor exato de $a(7)$ permaneça desconhecido, a resolução SAT pode navegar efetivamente no espaço de busca para encontrar caminhos significativamente mais longos do que os anteriormente descobertos, e que certificados de prova podem ser gerados para alegações de não existência.

Os autores permanecem modestos quanto à determinação de $a(7)$, observando que o valor exato ainda é desconhecido, mas esperam que sua introdução da resolução SAT a este problema facilite novos progressos.