Technische Samenvatting: Het breken van de symmetrieën van ononderscheidbare objecten

Probleemstelling

In constraint programming en verwante paradigma's bevatten problemen vaak ononderscheidbare objecten—entiteiten die uitwisselbaar zijn onder permutatie, zoals identieke machines in planning of golfers in het Social Golfer Problem. Wanneer deze objecten worden gemodelleerd met behulp van standaard gelabelde types (bijv. gehelen), moet de solver een zoekruimte verkennen die wordt opgeblazen door symmetrieën, waarbij het permuteren van de labels van ononderscheidbare objecten leidt tot equivalente oplossingen.

Hoewel symmetrie-doorbreking een goed bestudeerd onderwerp is in constraint satisfaction (CSP), Boolean satisfiability (SAT) en mixed-integer programming (MIP), hebben bestaande methoden vaak moeite met ononderscheidbare objecten wanneer deze voorkomen binnen complexe, geneste datastructuren (bijv. matrices geïndexeerd door ononderscheidbare objecten, verzamelingen van tupels, of functies). Hoogwaardige modellerings talen zoals Essence introduceren "onbenoemde types" om ononderscheidbare objecten abstract te representeren. Echter, eerdere implementaties van de automatische model herschrijvings tool Conjure negeerden de symmetrieën die inherent zijn aan onbenoemde types, door ze simpelweg te transformeren naar gehelen en de resulterende symmetrieën niet te breken. Dit artikel behandelt de uitdaging van het definiëren en breken van symmetrieën voor onbenoemde types binnen willekeurig geneste samengestelde types.

Methodologie

De auteurs stellen een framework voor om symmetrieën op onbenoemde types te definiëren en deze te breken met behulp van lex-leader constraints. De methodologie verloopt via de volgende theoretische en implementatiestappen:

1. Formele Definitie van Onbenoemde Types en Symmetrieën

Het artikel definieert een onbenoemd type $T$ van grootte $n$ als een verzameling waarden $\{1_T, 2_T, \dots, n_T\}$ uitgerust met de symmetrische groep $Sym(T)$ die op deze waarden werkt. In tegenstelling tot standaard types zijn de waarden van een onbenoemd type niet gelabeld en uitwisselbaar; de enige toegestane operaties zijn gelijkheid en ongelijkheid.

Om samengestelde types (matrices, multisets, tupels, functies, etc.) te behandelen die zijn geconstrueerd uit onbenoemde types, definiëren de auteurs een groepswerking recursief:

• Atomische waarden: Als een waarde van type $T$ is, wordt deze gepermuteerd door de groepswerking. Als het een ander atomisch type is, blijft deze onveranderd.
• Samengestelde structuren:
  • Matrices: De werking permuteert zowel de indices als de waarden. Cruciaal is dat voor een matrix $m$ geïndexeerd door $I$, de afbeelding $m^g$ bij index $i$ wordt gedefinieerd als $(m^{g^{-1}})_{i}^g$. Het gebruik van het pre-imago ($g^{-1}$) voor indices is noodzakelijk om ervoor te zorgen dat de werking een geldige groepshomomorfisme vormt.
  • Multisets en Tupels: De werking wordt elementgewijs toegepast.
  • Functies/Relaties: Behandeld als verzamelingen van tupels, de werking wordt toegepast op zowel domein- als codomein-elementen.

Voor meerdere verschillende onbenoemde types $T_1, \dots, T_m$ is de symmetriegroep de directe product $Sym(T_1) \times \dots \times Sym(T_m)$, werkend op de gezamenlijke oplossingsruimte.

2. Totale Ordening voor Symmetrie-doorbreking

Om symmetrieën volledig te breken, maakt het artikel gebruik van lex-leader constraints, die afdwingen dat een oplossing $X$ lexicografisch kleiner dan of gelijk aan zijn afbeelding onder een symmetrie $g$ moet zijn (d.w.z. $X \preceq X^g$). Dit vereist een totale ordening ($\preceq_T$) op de waarden van elk type $T$.

De auteurs definiëren een recursieve totale ordening voor alle Essence types die niet zijn geconstrueerd uit onbenoemde types:

• Atomische types: Standaard integer ordening, Boolean ordening ($false < true$), en enumeratie-orde.
• Samengestelde types:
  • Matrices/Tupels: Lexicografische ordening gebaseerd op de ordening van het innerlijke type.
  • Multisets: Een specifieke ordening gebaseerd op het minimale element en de recursieve vergelijking van de resterende multiset (vergelijkbaar met de "occurrence representation" ordening gevonden in de literatuur). Deze ordening is gekozen omdat deze aansluit bij de lexicografische ordening van een natuurlijke representatie van multisets.

3. Implementatie in Conjure

De methodologie is geïmplementeerd in Conjure, de automatische model herschrijvings tool voor Essence. Belangrijke implementatiekenmerken zijn:

• Nieuw permutation Type: Conjure introduceert een permutation domein constructor voor gehelen, geënumereerde types en onbenoemde types. Permutaties worden opgeslagen als bijectieve functies (matrices) samen met hun inversen om de toepassing van symmetrie-doorbrekingsconstraints te optimaliseren.
• Getagde Gehele Getallen: Tijdens de verfijning worden onbenoemde types omgezet naar gehelen maar behouden ze een "tag" die hun oorspronkelijke type aangeeft. Dit zorgt ervoor dat permutaties correct worden toegepast op de juiste set waarden over verschillende beslissingsvariabelen.
• Constraint Generatie: De tool genereert lex-leader constraints van de vorm $X \preceq transform(g, X)$ voor een gekozen deelverzameling van de symmetriegroep $G$.
  • Volledige Doorbreking: Gebruikt de volledige symmetrische groep (of direct product daarvan).
  • Partiële/Sound Doorbreking: Gebruikt deelverzamelingen van permutaties (bijv. alleen aangrenzende wisselingen of alle paren) om de kosten van constraint generatie af te wegen tegen de snelheid van het oplossen.
• Verfijning: De hoogwaardige ordeningsconstraints worden recursief verfijnd naar concrete constraints over atomische types (gehele getallen) en lexicografische vergelijkingen, waarbij vereenvoudigingsregels worden gebruikt om redundantie te verminderen.

Belangrijkste Bijdragen

1. Formele Semantiek voor Ononderscheidbare Objecten: Het artikel biedt een rigoureuze recursieve definitie van hoe symmetrieën op onbenoemde types symmetrieën induceren op willekeurig geneste samengestelde types (matrices, functies, verzamelingen, etc.), wat ambiguïteiten oplost in hoe permutaties werken op indices versus waarden.
2. Algemeen Framework voor Symmetrie-doorbreking: Het breidt de lex-leader methode uit om onbenoemde types binnen complexe datastructuren te behandelen, wat een algemene benadering biedt die toepasbaar is op elke modellerings taal die abstracte types ondersteunt.
3. Implementatie in Essence/Conjure: De auteurs bieden een volledige implementatie in Conjure, waarbij nieuwe types (permutation) en operatoren (image, transform) worden geïntroduceerd om deze symmetrieën automatisch te behandelen.
4. Flexibiliteit in Symmetrie-doorbreking: Het framework ondersteunt een spectrum van symmetrie-doorbrekingsstrategieën, van volledige doorbreking (garandeert exact één oplossing per equivalentieklasse) tot sound maar incomplete doorbreking (gebruik van deelverzamelingen van permutaties voor sneller oplossen).
5. Afleiding van Bekende Methoden: Het artikel toont aan dat gevestigde technieken, zoals de "double-lex" meth methode voor matrices geïndexeerd door twee onbenoemde types, natuurlijk voortkomen uit hun algemene framework.

Resultaten en Casestudy's

De auteurs valideren hun aanpak via verschillende casestudy's met onbenoemde types in diverse configuraties (samengevat in Tabel 1 van het artikel):

• Social Golfer Problem: Demonstreert het afhandelen van meerdere onbenoemde types (golfers, weken, groepen) in een matrix.
• Template Design Problem: Illustreert de noodzaak van consistente symmetrie-doorbreking over meerdere beslissingsvariabelen die dezelfde onbenoemde type index delen.
• Set-theoretic Yang-Baxter Problem: Een complexe casus waarbij een onbenoemd type zowel de index als het element van een matrix dient, wat gelijktijdige rij-, kolom- en waarde-permutaties vereist.
• Andere Problemen: Omvat Balanced Incomplete Block Designs, Covering Arrays, Rack Configuration, Semigroups en Sports Tournament Scheduling.

Verificatie:

• De resulterende modellen werden handmatig geïnspecteerd op correctheid.
• Voor kleine instanties van de Yang-Baxter en Semigroup problemen kwam het aantal gevonden oplossingen overeen met de bestaande literatuur, wat bevestigt dat de symmetrie-doorbreking correct was en geen geldige oplossingen heeft geëlimineerd.
• Het artikel merkt op dat volledige symmetrie-doorbreking voor bepaalde matrix types (bijv. $T \times T$) theoretisch even moeilijk is als het Grafen Isomorfisme probleem, wat verklaart waarom het aantal constraints groot kan zijn.

Betekenis en Claims

Het artikel claimt de eerste systematische methode te bieden voor het automatisch breken van symmetrieën voortvloeiend uit ononderscheidbare objecten in hoogwaardige modellerings talen wanneer deze objecten in complexe, geneste types zijn ingebed.

• Automatisering: Het elimineert de noodzaak voor handmatige modellerings expertise om symmetrieën te breken in problemen met onbenoemde types, een taak die voorheen veel inspanning vereiste en foutgevoelig was.
• Generaliteit: Door types te definiëren in termen van matrices, multisets en tupels, is de aanpak generaliseerbaar naar andere oplossings paradigma's en modellerings talen buiten Essence.
• Theoretische Fundering: Het werk dient als theoretische achtergrond voor toekomstig onderzoek door een recursieve semantiek voor type acties en groepswerkingen op samengestelde structuren vast te stellen.
• Bescheidenheid over Prestaties: De auteurs erkennen dat volledige symmetrie-doorbreking computationeel duur kan zijn (prohibitief in sommige gevallen) vanwege het enorme aantal vereiste constraints (gelinkt aan de complexiteit van grafen isomorfisme). Daarom benadrukken zij de waarde van hun framework in het bieden van partiële symmetrie-doorbrekingsopties, waardoor gebruikers kunnen kiezen tussen oplossingssnelheid en de volledigheid van symmetrie-eliminatie.

Het artikel concludeert door toekomstig werk te identificeren, waaronder het onderzoek naar representatie-specifieke totale ordeningen om de efficiëntie te verbeteren en de verkenning van symmetrie-doorbreking voor niet-symmetrische permutatiegroepen (bijv. schaakbord symmetrieën).