Constructing strong starters of orders $3p$: triplication with SAT solver

Este artigo apresenta uma abordagem inovadora chamada "triplicação" que utiliza um solucionador SAT (z3) para construir fortes iniciadores de ordem $3p$a partir de iniciadores de ordem$p$, abordando a conjectura de Horton sobre a existência desses objetos em grupos cíclicos de ordem divisível por 3.

O essencial

Imagine que você é um arquiteto de padrões matemáticos. O objetivo deste artigo é construir estruturas especiais chamadas "Starters Fortes" (ou "Iniciadores Fortes") dentro de grupos cíclicos.

Para entender o que isso significa, vamos usar uma analogia simples: o Sudoku e a Triplicação de Pizzas.

1. O Problema: O que é um "Starter Forte"?

Pense em um grupo de pessoas (números) que estão sentados em uma mesa redonda. Um "Starter" é uma maneira de emparelhar essas pessoas (excluindo o anfitrião, o número zero) de forma que:

1. As diferenças entre os pares sejam todas únicas (como se cada par tivesse uma "distância" única na mesa).
2. As somas dos pares também sejam todas únicas e não zero.

Um "Starter Forte" é um emparelhamento perfeito onde essas regras são seguidas rigorosamente. A matemática sabe que esses padrões existem para muitos tamanhos de mesa, mas há um mistério: o que acontece quando o número de lugares na mesa é um múltiplo de 3? (Ex: 21, 33, 39 lugares).

Há uma conjectura (uma suposição não provada) de que esses padrões existem para quase todos esses casos, mas ninguém sabia como construí-los de forma sistemática.

2. A Solução: A "Triplicação"

Os autores do artigo propõem um método novo e brilhante chamado Triplicação.

Imagine que você já tem uma mesa pequena e perfeita com 7 lugares (um "Starter Forte" de ordem 7). O objetivo é criar uma mesa gigante com 21 lugares (3 vezes maior) usando a mesa pequena como base.

A ideia é como se você tivesse uma receita de pizza:

• Você pega sua pizza base (a mesa de 7).
• Você quer fazer uma pizza gigante (a mesa de 21).
• Em vez de tentar adivinhar onde colocar cada ingrediente na pizza gigante (o que seria um pesadelo), você usa a pizza pequena como molde.

3. O Segredo: O "Sudoku Modulo 3"

Aqui entra a parte mágica. Para transformar a pizza de 7 em uma de 21, os autores criam um problema que parece um Sudoku, mas muito mais simples e estranho:

• Em vez de números de 1 a 9, usamos apenas 0, 1 e 2.
• A "pizza base" (de 7 lugares) nos diz como organizar os ingredientes principais.
• O "Sudoku" nos diz como preencher os detalhes finos para que a pizza gigante funcione.

Se você conseguir resolver esse Sudoku (encontrar uma combinação de 0s, 1s e 2s que obedeça às regras), você pode usar uma ferramenta matemática antiga chamada Teorema do Resto Chinês para "costurar" a mesa pequena e o Sudoku juntos. O resultado é a mesa gigante perfeita de 21 lugares!

4. O Detetive e o SAT Solver

Resolver esse Sudoku manualmente é difícil e demorado. Então, os autores usaram um "detetive de computador" chamado SAT Solver (especificamente o programa z3).

• O SAT Solver é como um super-robô que testa milhões de combinações em segundos para ver se existe uma solução que satisfaça todas as regras.
• Eles ensinaram ao robô as regras do Sudoku e deixaram que ele encontrasse o padrão.
• Funcionou! O robô encontrou soluções rapidamente para mesas de até 500 lugares.

5. Analogia Final: O Código Secreto

Pense no "Starter Forte" como um código secreto que precisa ser enviado por rádio.

• A mesa pequena (ordem 7) é a mensagem original.
• O problema do Sudoku (ordem 3) é a chave de criptografia.
• A mesa grande (ordem 21) é a mensagem criptografada que chega ao destino.

Os autores descobriram que, se você tiver a mensagem original e a chave certa (o Sudoku resolvido), pode gerar a mensagem criptografada gigante sem precisar inventar tudo do zero. Eles provaram que, na maioria dos casos, essa chave existe e o robô consegue achá-la.

Resumo em uma frase

O artigo apresenta um método inteligente para criar padrões matemáticos complexos em grandes grupos (múltiplos de 3) pegando um padrão menor, resolvendo um quebra-cabeça simples de 3 cores (como um mini-Sudoku) com a ajuda de um computador, e juntando tudo para formar o padrão gigante perfeito.

Isso é importante porque resolve um quebra-cabeça matemático que estava parado desde 1989, mostrando que esses padrões "fortes" provavelmente existem em todos os lugares onde a matemática diz que deveriam, e nos dando uma ferramenta prática para encontrá-los.

Resumo técnico

Título: Construção de Starters Fortes de Ordens $3p$: Triplicação com Solucionador SAT

Autores: Oleg Ogandzhanyants, Sergey Sadov e Margo Kondratieva.
Instituições: Memorial University (Canadá) e Moscou (Rússia).

---

1. O Problema

O artigo aborda a construção de starters fortes (um tipo específico de design combinatório) em grupos cíclicos $\mathbb{Z}_n$, onde $n$ é um número ímpar divisível por 3 (ou seja, $n = 3p$).

• Definição de Starter Forte: Um starter em um grupo abeliano de ordem ímpar $n$ é uma partição do conjunto $G \setminus \{0\}$ em pares $\{a_i, b_i\}$ tal que as diferenças $\pm(a_i - b_i)$ cobrem todos os elementos não nulos do grupo. Um starter é considerado forte se, além disso, as somas dos pares $a_i + b_i$ forem todas distintas e não nulas módulo $n$.
• O Desafio Teórico: A existência de starters fortes é bem estabelecida para ordens $n$ onde 3 não divide $n$. No entanto, para ordens $n$ divisíveis por 3 (exceto $n=3$ e $n=9$), a existência é objeto da Conjectura de Horton (1989), que afirma que eles existem, mas permanece não provada teoricamente para casos gerais onde $n = 3p$ e $p > 333$ (ou limites superiores similares).
• Lacuna: Não há métodos construtivos gerais conhecidos para gerar starters fortes de ordem $3p$a partir de *starters* de ordem$p$, especialmente quando$p$ é primo ou coprimo com 3.

2. Metodologia: O Método de Triplicação

Os autores propõem um novo método construtivo chamado "Triplicação". A ideia central é transformar o problema de encontrar um starter forte de ordem $3p$ em um problema de satisfação de restrições (CSP) modular, especificamente um tipo de Sudoku módulo 3.

O processo funciona da seguinte forma:

1. Entrada:

   • Um starter forte de ordem $p$ (onde $\gcd(p, 3) = 1$), denotado por $T$.
   • Uma "chave" numérica $t \in \{0, \dots, p-1\}$.

2. Construção da Tabela $\Sigma_p$ (Triplicação):

   • A partir de $T$ e da chave $t$, constrói-se uma tabela de triplicação $\Sigma_p$ com 3 colunas e $q+1$ linhas (onde $q = (p-1)/2$).
   • A primeira coluna é uma cópia do starter base $T$.
   • A segunda coluna é gerada somando $t$ aos elementos de $T$.
   • A terceira coluna é gerada por uma transformação específica envolvendo $t$ e a inversão dos elementos de $T$.
   • O topo da segunda coluna contém o par $(t, t)$.

3. O Problema do Sudoku Modular ($\Sigma_3$):

   • O objetivo é preencher uma tabela correspondente $\Sigma_3$ com valores $\{0, 1, 2\}$ (módulo 3) para cada posição da tabela $\Sigma_p$.
   • As variáveis são $U_i, V_i$ (os valores módulo 3 dos pares da tabela estendida).
   • Restrições Imostas:
     • Restrições de Linha: As diferenças $U_i - V_i$ em cada linha regular devem ser distintas módulo 3 (formando o conjunto $\{0, 1, 2\}$).
     • Restrições de Conjuntos Fracos (Weak Sets): Pares na tabela $\Sigma_p$ que têm a mesma soma módulo $p$ devem ter somas distintas (e não nulas, se a soma em $p$ for zero) módulo 3.
     • Restrições de Cores (Monochrome Sets): Posições na tabela $\Sigma_p$ que contêm o mesmo valor numérico $c$ devem receber valores distintos módulo 3.

4. Resolução e Reconstrução:

   • O problema de preencher $\Sigma_3$ é resolvido usando um Solver SAT (especificamente a biblioteca z3 da Microsoft).
   • Se uma solução para $\Sigma_3$ existe, ela é combinada com a tabela $\Sigma_p$ usando o Teorema Chinês do Resto (CRT) para reconstruir um starter forte de ordem $3p$.

3. Contribuições Principais

1. Novo Método Construtivo: Introdução do método de "triplicação", que reduz a construção de starters de ordem $3p$ para a solução de um sistema de equações lineares e desigualdades módulo 3.
2. Formulação como Problema SAT: Demonstração prática de que o problema de preenchimento da tabela modular pode ser modelado e resolvido eficientemente usando solucionadores SAT de propósito geral.
3. Resultados Teóricos:
   • Teorema 1: Prova que qualquer solução válida do problema do Sudoku modular gera um starter forte de ordem $3p$.
   • Teorema 2: Estabelece uma condição necessária para a solvabilidade: a chave $t$ não pode ser 0 nem pertencer ao conjunto de somas dos pares do starter base $T$.
   • Teorema 3: Demonstra uma simetria involutiva nas soluções (permutação dos valores 1 e 2 módulo 3 gera outra solução válida).
   • Algoritmo de Reconhecimento: Apresenta um critério (baseado na estrutura de linhas da tabela) para determinar se um starter de ordem $3p$ não pode ter sido obtido por triplicação.
4. Validação Empírica: Implementação completa em Python e testes extensivos para ordens de $p$ até 499.

4. Resultados Experimentais

Os autores realizaram três séries de experimentos numéricos utilizando o solver z3:

• Série 1 (Ordens < 100): Testaram todos os starters fortes de ordem $p < 100$ e todas as chaves admissíveis.
  • O tempo de execução médio cresceu aproximadamente de forma quadrática logarítmica ($\tau \approx m^2 \ln m$).
  • Para $p=7$, o tempo foi de ~0.06s; para $p=97$, ~90s.
• Série 2 (Ordens 100 a 500): Testaram ordens maiores com chaves aleatórias.
  • Observou-se que para $m > 200$, o tempo de execução aumentou mais rapidamente do que a previsão teórica simples, com saltos dramáticos (ex: de 335 para 395).
  • Apesar da não monotonicidade, os dados não refutam a hipótese de um limite polinomial para o tempo de solução.
• Série 3 (Variação de Chaves): Para uma ordem fixa ($m=101$), testaram 50 chaves diferentes, cada uma 10 vezes.
  • Houve uma variação significativa no tempo de execução dependendo da chave escolhida (de ~83s a ~260s), sugerindo que a estrutura do problema varia com a chave, mesmo para o mesmo starter base.

Comparação de Desempenho:

• O método de triplicação com SAT é muito mais rápido do que tentar encontrar um starter forte de ordem $3p$ diretamente com SAT (ex: ordem 39 leva ~200s diretamente vs <1s via triplicação).
• No entanto, o método de hill-climbing (algoritmo de Dinitz-Stinson) ainda é mais rápido para gerar starters aleatórios (menos de 2.5s para 1000 amostras de ordem 39), embora a triplicação ofereça uma abordagem construtiva sistemática baseada em starters menores.

5. Significado e Conclusão

• Avanço Teórico: O trabalho fornece uma ferramenta poderosa para investigar a Conjectura de Horton. Ao permitir a construção sistemática de starters de ordem $3p$ a partir de ordens menores, ele expande o conhecimento sobre a existência desses objetos combinatórios.
• Aplicabilidade Prática: A demonstração de que solucionadores SAT modernos podem resolver eficientemente problemas de "Sudoku modular" abre caminho para a aplicação de técnicas de satisfação de restrições em outros problemas de design combinatório.
• Limitações e Futuro: Os autores notam que a solução atual depende de um solver genérico. Eles planejam desenvolver um algoritmo especializado para resolver o problema do Sudoku modular, o que deve superar significativamente o desempenho do solver SAT e o método de hill-climbing.
• Descoberta de Não-Triplicação: O estudo revelou que a maioria dos starters fortes "aleatórios" de ordem $3p$ não pode ser obtida por triplicação, indicando que o método de triplicação gera um subconjunto específico (embora grande) dos starters possíveis.

Em resumo, o artigo apresenta uma ponte elegante entre a teoria dos grupos, designs combinatórios e a computação moderna (SAT solvers), oferecendo um método viável para construir starters fortes em ordens anteriormente difíceis de tratar teoricamente.