Resumo Técnico: Quebrando as Simetrias de Objetos Indistinguíveis

Definição do Problema

Em programação de restrições e paradigmas relacionados, os problemas frequentemente envolvem objetos indistinguíveis — entidades que são equivalentes sob intercâmbio, como máquinas idênticas em escalonamento ou golfistas no Problema do Golfer Social. Quando esses objetos são modelados usando tipos rotulados padrão (por exemplo, inteiros), o solver deve explorar um espaço de busca inflado por simetrias, onde a permutação dos rótulos de objetos indistinguíveis produz soluções equivalentes.

Embora a quebra de simetria seja um tema bem estudado em satisfação de restrições (CSP), satisfatibilidade booleana (SAT) e programação inteira mista (MIP), os métodos existentes frequentemente têm dificuldades com objetos indistinguíveis quando estes aparecem dentro de estruturas de dados complexas e aninhadas (por exemplo, matrizes indexadas por objetos indistinguíveis, conjuntos de tuplas ou funções). Linguagens de modelagem de alto nível como Essence introduzem "tipos sem nome" para representar abstratamente esses objetos indistinguíveis. No entanto, implementações anteriores da ferramenta de reescrita automática de modelos Conjure ignoraram as simetrias inerentes aos tipos sem nome, transformando-os simplesmente em inteiros e falhando em quebrar as simetrias resultantes. Este artigo aborda o desafio de definir e quebrar simetrias para tipos sem nome dentro de tipos compostos arbitrariamente aninhados.

Metodologia

Os autores propõem um framework para definir simetrias em tipos sem nome e quebrá-las usando restrições de lex-leader. A metodologia procede através de etapas teóricas e de implementação fundamentais:

1. Definição Formal de Tipos Sem Nome e Simetrias

O artigo define um tipo sem nome $T$ de tamanho $n$ como um conjunto de valores $\{1_T, 2_T, \dots, n_T\}$ equipado com o grupo simétrico $Sym(T)$ atuando sobre esses valores. Diferente de tipos padrão, os valores de um tipo sem nome são não rotulados e intercambiáveis; a única operação permitida é igualdade e desigualdade.

Para lidar com tipos compostos (matrizes, multiconjuntos, tuplas, funções, etc.) construídos a partir de tipos sem nome, os autores definem uma ação de grupo recursivamente:

• Valores atômicos: Se um valor é de tipo $T$, ele é permutado pela ação do grupo. Se for de um tipo atômico diferente, permanece fixo.
• Estruturas compostas:
  • Matrizes: A ação permuta tanto os índices quanto os valores. Crucialmente, para uma matriz $m$ indexada por $I$, a imagem $m^g$ no índice $i$ é definida como $(m^{g^{-1}})_{i}^g$. O uso do pré-imagem ($g^{-1}$) para os índices é necessário para garantir que a ação forme um homomorfismo de grupo válido.
  • Multiconjuntos e Tuplas: A ação é aplicada elemento a elemento.
  • Funções/Relações: Tratadas como conjuntos de tuplas, a ação aplica-se tanto ao domínio quanto ao codomínio.

Para múltiplos tipos sem nome distintos $T_1, \dots, T_m$, o grupo de simetria é o produto direto $Sym(T_1) \times \dots \times Sym(T_m)$, atuando no espaço de solução conjunto.

2. Ordenação Total para Quebra de Simetria

Para quebrar as simetrias completamente, o artigo emprega restrições de lex-leader, que impõem que uma solução $X$ deve ser lexicograficamente menor ou igual à sua imagem sob qualquer simetria $g$ (ou seja, $X \preceq X^g$). Isso requer uma ordenação total ($\preceq_T$) nos valores de cada tipo $T$.

Os autores definem uma ordenação total recursiva para todos os tipos Essence que não são construídos a partir de tipos sem nome:

• Tipos atômicos: Ordenação padrão de inteiros, ordenação booleana ($false < true$) e ordem de enumeração.
• Tipos compostos:
  • Matrizes/Tuplas: Ordenação lexicográfica baseada na ordenação do tipo interno.
  • Multiconjuntos: Uma ordenação específica baseada no elemento mínimo e na comparação recursiva do multiconjunto restante (semelhante à ordenação de "representação de ocorrência" encontrada na literatura). Esta ordenação é escolhida porque se alinha com a ordenação lexicográfica de uma representação natural de multiconjuntos.

3. Implementação no Conjure

A metodologia é implementada no Conjure, a ferramenta de reescrita automática de modelos para Essence. Principais características da implementação incluem:

• Novo Tipo permutation: O Conjure introduz um construtor de domínio permutation para inteiros, tipos enumerados e tipos sem nome. As permutações são armazenadas como funções bijetivas (matrizes) junto com suas inversas para otimizar a aplicação das restrições de quebra de simetria.
• Inteiros Etiquetados (Tagged Integers): Durante o refinamento, os tipos sem nome são convertidos em inteiros, mas retêm uma "etiqueta" indicando seu tipo original. Isso garante que as permutações sejam aplicadas corretamente ao conjunto correto de valores entre diferentes variáveis de decisão.
• Geração de Restrições: A ferramenta gera restrições de lex-leader da forma $X \preceq transform(g, X)$ para um subconjunto escolhido do grupo de simetria $G$.
  • Quebra Completa: Utiliza o grupo simétrico total (ou o produto direto deles).
  • Quebra Parcial/Sons: Utiliza subconjuntos de permutações (por exemplo, apenas trocas adjacentes ou todos os pares) para equilibrar o custo de geração de restrições com a velocidade de resolução.
• Refinamento: As restrições de ordenação de alto nível são refinadas recursivamente em restrições concretas sobre tipos atômicos (inteiros) e comparações lexicográficas, utilizando regras de simplificação para reduzir a redundância.

Principais Contribuições

1. Semântica Formal para Objetos Indistinguíveis: O artigo fornece uma definição recursiva rigorosa de como as simetrias em tipos sem nome induzem simetrias em tipos compostos arbitrariamente aninhados (matrizes, funções, conjuntos, etc.), resolvendo ambiguidades sobre como as permutações atuam nos índices versus nos valores.
2. Framework Geral de Quebra de Simetria: Estende o método de lex-leader para lidar com tipos sem nome dentro de estruturas de dados complexas, oferecendo uma abordagem geral aplicável a qualquer linguagem de modelagem que suporte tipos abstratos.
3. Implementação em Essence/Conjure: Os autores fornecem uma implementação completa no Conjure, introduzindo novos tipos (permutation) e operadores (image, transform) para lidar com essas simetrias automaticamente.
4. Flexibilidade na Quebra de Simetria: O framework suporta um espectro de estratégias de quebra de simetria, desde a quebra completa (garantindo exatamente uma solução por classe de equivalência) até a quebra sons mas incompleta (usando subconjuntos de permutações para uma resolução mais rápida).
5. Derivação de Métodos Conhecidos: O artigo demonstra que técnicas estabelecidas, como o método "double-lex" para matrizes indexadas por dois tipos sem nome, surgem naturalmente de seu framework geral.

Resultados e Estudos de Caso

Os autores validam sua abordagem através de vários estudos de caso envolvendo tipos sem nome em várias configurações (resumidos na Tabela 1 do artigo):

• Problema do Golfer Social: Demonstra o tratamento de múltiplos tipos sem nome (golfistas, semanas, grupos) em uma matriz.
• Problema de Design de Template: Ilustra a necessidade de uma quebra de simetria consistente entre múltiplas variáveis de decisão que compartilham o mesmo índice de tipo sem nome.
• Problema de Yang-Baxter Teórico-Conjunto: Um caso complexo onde um tipo sem nome serve tanto como índice quanto como elemento de uma matriz, exigindo permutações simultâneas de linha, coluna e valor.
• Outros Problemas: Inclui Blocos Incompletos Balanceados, Matrizes de Cobertura, Configuração de Rack, Semigrupos e Escalonamento de Torneios Esportivos.

Verificação:

• Os modelos resultantes foram inspecionados manualmente para correção.
• Para instâncias pequenas dos problemas de Yang-Baxter e Semigrupos, o número de soluções encontradas coincidiu com a literatura existente, confirmando que a quebra de simetria foi correta e não eliminou soluções válidas.
• O artigo observa que a quebra de simetria completa para certos tipos de matriz (por exemplo, $T \times T$) é teoricamente tão difícil quanto o problema de Isomorfismo de Grafos, explicando por que o número de restrições pode ser grande.

Significância e Alegações

O artigo afirma fornecer o primeiro método sistemático para quebrar automaticamente simetrias decorrentes de objetos indistinguíveis em linguagens de modelagem de alto nível quando esses objetos estão incorporados em tipos compostos e aninhados.

• Automação: Remove a necessidade de expertise manual de modelagem para quebrar simetrias em problemas envolvendo tipos sem nome, uma tarefa que anteriormente exigia esforço significativo e era propensa a erros.
• Generalidade: Ao definir tipos em termos de matrizes, multiconjuntos e tuplas, a abordagem é generalizável para outros paradigmas de resolução e linguagens de modelagem além do Essence.
• Fundamentação Teórica: O trabalho serve como um pano de fundo teórico para pesquisas futuras, estabelecendo uma semântica recursiva para ações de tipos e ações de grupo em estruturas compostas.
• Modéstia sobre Desempenho: Os autores reconhecem que a quebra de simetria completa pode ser computacionalmente cara (proibitivamente, em alguns casos) devido ao enorme número de restrições necessárias (ligado à complexidade do isomorfismo de grafos). Consequentemente, eles enfatizam o valor de seu framework em oferecer opções de quebra de simetria parcial, permitindo que os usuários escolham entre velocidade de resolução e a completude da eliminação de simetria.

O artigo conclui identificando trabalhos futuros, incluindo a investigação de ordenações totais específicas de representação para melhorar a eficiência e a exploração de quebra de simetria para grupos de permutação não simétricos (por exemplo, simetrias de tabuleiro de xadrez).