Exact Zarankiewicz Values On Two Finite Frontier Slices

Resumo Técnico: Valores Exatos de Zarankiewicz em Duas Fatias de Fronteira Finitas

Enunciado do Problema
O artigo aborda o problema de Zarankiewicz, que busca o número máximo de arestas, denotado por $Z(m, n, s, t)$, em um grafo bipartido com partes de tamanho $m$ e $n$ que não contém um subgrafo bipartido completo $K_{s,t}$. O autor foca especificamente no caso $s=t=3$ (evitando $K_{3,3}$) para parâmetros finitos moderados. Embora a teoria assintótica esteja bem desenvolvida, os valores exatos para dimensões finitas específicas permanecem difíceis devido à severa simetria e ao alto custo de certificação de prova. O artigo visa uma "fronteira finita" de valores anteriormente não resolvidos ou parcialmente resolvidos, incluindo a faixa $Z(12, n, 3, 3)$ para $18 \le n \le 22$, o caso específico $Z(13, 22, 3, 3)$, e um aglomerado de valores vizinhos em torno de $13 \times 18$ e $16 \times 17$.

Metodologia
A prova é assistida por computador, mas estritamente baseada em certificados, distinguindo-se de métodos que dependem apenas de solvers de programação linear inteira mista (MILP) que retornam "inviável" ou de solvers SAT sem testemunhas explícitas. A verificação baseia-se em aritmética exata de inteiros e racionais (usando Fraction do Python e bibliotecas padrão), com otimização de ponto flutuante utilizada apenas para a descoberta inicial de certificados.

A metodologia emprega uma estratégia de redução em múltiplas camadas:

1. Relaxação Global e Perfis de Grau: Para o caso $13 \times 22$, o autor assume uma matriz hipotética com 138 arestas. Ao analisar a função de "penalidade" $p(d) = \binom{d}{3} - 15d + 70$ associada aos graus das colunas, o espaço de busca é reduzido de todas as matrizes possíveis para apenas 83 perfis de grau distintos (histogramas de graus de coluna).
2. Certificados de Farkas: Para 77 dos 83 perfis, o autor constrói certificados de Farkas racionais exatos. Esses certificados provam a inviabilidade ao demonstrar que as restrições lineares impostas pela condição livre de $K_{3,3}$ (especificamente, que cada tripla de linhas aparece em no máximo 2 colunas) não podem ser satisfeitas por qualquer solução inteira não negativa para aquele perfil.
3. Enumeração de Linha Marcada e Resto (Leave): Os seis perfis restantes são excluídos usando técnicas mais granulares, nas quais o autor fixa uma "linha marcada", deleta-a e analisa o "multigrafo resto" resultante nos 12 pontos restantes. Isso envolve:
   • Argumentos de Congruência: Usando aritmética modular sobre déficits de linhas para excluir configurações específicas (ex: perfil 6187391).
   • Restrições de Matriz de Gram: Verificação de condições de posto (rank) e determinante da matriz de incidência de blocos residuais.
   • Enumeração Exata: Enumeração exaustiva de designs de blocos residuais e aplicação de certificados de Farkas com escala inteira para os sistemas de fatoração restantes.
4. Lemas de Deleção e Testemunhas: Para a faixa $12 \times n$ e o fechamento da fronteira, o autor utiliza "lemas de deleção" (relacionando $Z(m, n)$ a $Z(m, n-1)$) combinados com testemunhas construtivas explícitas (matrizes que alcançam os limites inferiores) para estabelecer igualdades exatas.

Principos Contribuições e Resultados
O artigo fornece uma prova combinada, baseada em certificados, para os seguintes valores e limites exatos:

• A Faixa $12 \times n$: Prova que $Z(12, n, 3, 3) = 6n$ para $18 \le n \le 22$. Isso é estabelecido por um certificado exato para $Z(12, 18, 3, 3) = 108$ e argumentos de deleção subsequentes apoiados por testemunhas explícitas para $n=19, 20, 21, 22$.
• O Caso $13 \times 22$: Prova que $Z(13, 22, 3, 3) = 137$. O limite superior de 138 é eliminado pela análise de perfil exaustiva descrita acima. Um limite inferior de 137 é confirmado via uma construção explícita (uma matriz binária $13 \times 22$ com 137 uns e sem $K_{3,3}$).
• Fechamento da Fronteira: Estabelece valores exatos para quatro células vizinhas:
  • $Z(13, 18, 3, 3) = 116$
  • $Z(14, 17, 3, 3) = 118$
  • $Z(14, 18, 3, 3) = 124$
  • $Z(15, 17, 3, 3) = 126$
  • $Z(15, 18, 3, 3) = 132$
• O Intervalo $16 \times 17$: Relata o intervalo $132 \le Z(16, 17, 3, 3) \le 133$. O limite inferior é suportado por uma nova testemunha de 132 arestas; o limite superior de 133 é tomado da literatura prévia (Collins et al.). O artigo nota explicitamente que o valor exato para esta célula específica não é determinado neste trabalho.

Significância e Alegações
O autor afirma que este trabalho fornece uma prova completa, reproduzível e baseada em certificados para estes valores específicos de Zarankiewicz. A significância reside na separação rigorosa entre a descoberta (onde heurísticas de ponto flutuante podem ser usadas) e a verificação (que utiliza apenas aritmética exata).

• Reproduzibilidade: O artigo inclui um "portão de verificação de um comando" que reproduz todos os 5,7 milhões de verificações de não-negatividade exatas, incluindo a regeneração de perfis de grau, a reprodução de certificados de Farkas e a enumeração exaustiva de designs de blocos residuais.
• Modéstia: O autor afirma explicitamente que estes resultados devem ser considerados "novas provas assistidas por computador pendentes de reprodução independente e revisão por pares". O artigo não pretende resolver o problema geral de Zarankiewicz ou fornecer um algoritmo universal, mas demonstra uma divisão de trabalho para problemas extremos finitos: usar relaxações globais grosseiras para eliminar a maioria dos casos e reservar a enumeração exata, computacionalmente intensiva, para os poucos perfis residuais "difíceis".
• Arte Prévia: O autor observa que, embora a construção de 137 arestas para $13 \times 22$ tenha sido reportada anteriormente, o limite superior exato é uma nova contribuição. Da mesma forma, os valores específicos para a faixa $12 \times n$ ($n=18$ a $21$) e os valores de fechamento da fronteira são reportados como novos resultados exatos não encontrados na literatura indexada anterior à data do artigo (agosto de 2026).

O artigo conclui enfatizando que nenhuma alegação de DRAT não verificada, timeouts de SAT ou status de solvers de ponto flutuante são usados como premissas para os teoremas, garantindo que as alegações matemáticas repousem inteiramente em dados finitos explícitos e aritmética exata.