🤖 AI

Breaking the Symmetries of Indistinguishable Objects

This paper presents a method for correctly defining and breaking symmetries arising from indistinguishable objects within complex types, implemented through "unnamed types" in the high-level modelling language Essence.

Original authors: Ozgur Akgun, Mun See Chang, Ian P. Gent, Christopher Jefferson

Published 2026-07-30

📖 3 min read☕ Coffee break read

CC BY 4.0

Original authors: Ozgur Akgun, Mun See Chang, Ian P. Gent, Christopher Jefferson

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to solve a massive, intricate puzzle, but the pieces are all made of the exact same clay. They look identical, they feel identical, and if you swap two of them, the picture doesn't change at all. In the world of computer science, specifically a field called "constraint programming," this is a common headache. Computers are incredibly fast at crunching numbers, but they are terrible at realizing when they are doing the exact same work twice. If a computer thinks it has found a solution, but then swaps two identical "indistinguishable" objects and finds another solution that is actually just a copy of the first one, it wastes precious time exploring a dead end. This is called a "symmetry," and it's like a computer running in circles, checking the same door over and over again because it can't tell the difference between the handle and the knob.

To stop this, mathematicians and computer scientists use "symmetry breaking." Think of it as a strict rulebook that says, "Okay, we know these pieces are identical, but for the sake of efficiency, we will pretend the red one is always on the left and the blue one is always on the right." This forces the computer to pick just one version of the solution and ignore all the identical copies. However, things get tricky when these identical objects are nested inside complex structures, like a matrix (a grid) or a list of lists. Until now, computers struggled to apply these rules when the identical objects were hidden deep inside these layers, often leading to confusion or missed solutions.

This paper, titled "Breaking the Symmetries of Indistinguishable Objects," introduces a clever new way to teach computers how to handle these tricky, nested identical objects. The authors, working with a high-level modeling language called Essence and a tool called Conjure, have developed a system that automatically recognizes when objects are indistinguishable, even when they are buried inside complex data structures. They created a new mathematical "total ordering"—a fancy way of saying they invented a universal rule for deciding which identical object comes "first" in a lineup, no matter how deep it is hidden. By applying this rule, their system can automatically generate constraints that tell the computer to ignore all the duplicate solutions and focus only on the unique ones.

The authors demonstrate that this method works by testing it on several classic problems, like the "Social Golfers Problem" (where you have to schedule golfers into groups without them playing together twice) and the "Template Design Problem" (figuring out how to print designs on sheets of paper). In these tests, their new method successfully broke the symmetries, ensuring the computer didn't waste time on duplicate schedules. They also showed that you can choose how strict you want to be: you can break all symmetries to get a perfect, unique list of solutions, or you can use a "partial" method that breaks just enough symmetries to make the computer run faster, trading a little bit of completeness for a lot of speed. The paper confirms that while this approach is powerful, it can sometimes generate a huge number of rules, which might slow things down for very complex problems, suggesting that finding the perfect balance between speed and strictness is an area for future exploration.

Technical Summary: Breaking the Symmetries of Indistinguishable Objects

Problem Statement

In constraint programming and related paradigms, problems often involve indistinguishable objects—entities that are equivalent under interchange, such as identical machines in scheduling or golfers in the Social Golfer Problem. When these objects are modeled using standard labeled types (e.g., integers), the solver must explore a search space inflated by symmetries, where permuting the labels of indistinguishable objects yields equivalent solutions.

While symmetry breaking is a well-studied topic in constraint satisfaction (CSP), Boolean satisfiability (SAT), and mixed-integer programming (MIP), existing methods often struggle with indistinguishable objects when they appear within complex, nested data structures (e.g., matrices indexed by indistinguishable objects, sets of tuples, or functions). High-level modeling languages like Essence introduce "unnamed types" to abstractly represent these indistinguishable objects. However, previous implementations of the automatic model rewriting tool Conjure ignored the symmetries inherent in unnamed types, simply transforming them into integers and failing to break the resulting symmetries. This paper addresses the challenge of defining and breaking symmetries for unnamed types within arbitrarily nested compound types.

Methodology

The authors propose a framework to define symmetries on unnamed types and break them using lex-leader constraints. The methodology proceeds through several key theoretical and implementation steps:

1. Formal Definition of Unnamed Types and Symmetries

The paper defines an unnamed type $T$ of size $n$ as a set of values $\{1_T, 2_T, \dots, n_T\}$ equipped with the symmetric group $Sym(T)$ acting on these values. Unlike standard types, the values of an unnamed type are unlabelled and interchangeable; the only allowed operations are equality and inequality.

To handle compound types (matrices, multisets, tuples, functions, etc.) constructed from unnamed types, the authors define a group action recursively:

Atomic values: If a value is of type $T$ , it is permuted by the group action. If it is of a different atomic type, it remains fixed.
Compound structures:
- Matrices: The action permutes both the indices and the values. Crucially, for a matrix $m$ indexed by $I$ , the image $m^g$ at index $i$ is defined as $(m^{g^{-1}})_{i}^g$ . The use of the preimage ( $g^{-1}$ ) for indices is necessary to ensure the action forms a valid group homomorphism.
- Multisets and Tuples: The action applies element-wise.
- Functions/Relations: Treated as sets of tuples, the action applies to both domain and codomain elements.

For multiple distinct unnamed types $T_1, \dots, T_m$ , the symmetry group is the direct product $Sym(T_1) \times \dots \times Sym(T_m)$ , acting on the joint solution space.

2. Total Ordering for Symmetry Breaking

To break symmetries completely, the paper employs lex-leader constraints, which enforce that a solution $X$ must be lexicographically smaller than or equal to its image under any symmetry $g$ (i.e., $X \preceq X^g$ ). This requires a total ordering ( $\preceq_T$ ) on the values of every type $T$ .

The authors define a recursive total ordering for all Essence types not constructed from unnamed types:

Atomic types: Standard integer ordering, Boolean ordering ($false < true$), and enumeration order.
Compound types:
- Matrices/Tuples: Lexicographic ordering based on the ordering of the inner type.
- Multisets: A specific ordering based on the minimum element and recursive comparison of the remaining multiset (similar to the "occurrence representation" ordering found in literature). This ordering is chosen because it aligns with lexicographic ordering of a natural representation of multisets.

3. Implementation in Conjure

The methodology is implemented in Conjure, the automatic model rewriting tool for Essence. Key implementation features include:

New permutation Type: Conjure introduces a permutation domain constructor for integers, enumerated types, and unnamed types. Permutations are stored as bijective functions (matrices) along with their inverses to optimize the application of symmetry breaking constraints.
Tagged Integers: During refinement, unnamed types are converted to integers but retain a "tag" indicating their original type. This ensures that permutations are applied correctly to the correct set of values across different decision variables.
Constraint Generation: The tool generates lex-leader constraints of the form $X \preceq transform(g, X)$ $X ⪯ t r an s f or m (g, X)$ for a chosen subset of the symmetry group $G$ $G$ .
- Complete Breaking: Uses the full symmetric group (or direct product thereof).
- Partial/Sound Breaking: Uses subsets of permutations (e.g., only adjacent swaps or all pairs) to trade off constraint generation cost for solving speed.
Refinement: The high-level ordering constraints are recursively refined into concrete constraints over atomic types (integers) and lexicographic comparisons, utilizing simplification rules to reduce redundancy.

Key Contributions

Formal Semantics for Indistinguishable Objects: The paper provides a rigorous recursive definition of how symmetries on unnamed types induce symmetries on arbitrarily nested compound types (matrices, functions, sets, etc.), resolving ambiguities in how permutations act on indices versus values.
General Symmetry Breaking Framework: It extends the lex-leader method to handle unnamed types within complex data structures, offering a general approach applicable to any modeling language that supports abstract types.
Implementation in Essence/Conjure: The authors provide a complete implementation in Conjure, introducing new types (permutation) and operators (image, transform) to handle these symmetries automatically.
Flexibility in Symmetry Breaking: The framework supports a spectrum of symmetry breaking strategies, from complete breaking (guaranteeing exactly one solution per equivalence class) to sound but incomplete breaking (using subsets of permutations for faster solving).
Derivation of Known Methods: The paper demonstrates that established techniques, such as the "double-lex" method for matrices indexed by two unnamed types, naturally arise from their general framework.

Results and Case Studies

The authors validate their approach through several case studies involving problems with unnamed types in various configurations (summarized in Table 1 of the paper):

Social Golfer Problem: Demonstrates handling of multiple unnamed types (golfers, weeks, groups) in a matrix.
Template Design Problem: Illustrates the need for consistent symmetry breaking across multiple decision variables sharing the same unnamed type index.
Set-theoretic Yang-Baxter Problem: A complex case where an unnamed type serves as both the index and the element of a matrix, requiring simultaneous row, column, and value permutations.
Other Problems: Includes Balanced Incomplete Block Designs, Covering Arrays, Rack Configuration, Semigroups, and Sports Tournament Scheduling.

Verification:

The resulting models were manually inspected for correctness.
For small instances of the Yang-Baxter and Semigroup problems, the number of solutions found matched existing literature, confirming that the symmetry breaking was correct and did not eliminate valid solutions.
The paper notes that complete symmetry breaking for certain matrix types (e.g., $T \times T$ ) is theoretically as hard as the Graph Isomorphism problem, explaining why the number of constraints can be large.

Significance and Claims

The paper claims to provide the first systematic method for automatically breaking symmetries arising from indistinguishable objects in high-level modeling languages when these objects are embedded in complex, nested types.

Automation: It removes the need for manual modeling expertise to break symmetries in problems involving unnamed types, a task that previously required significant effort and was error-prone.
Generality: By defining types in terms of matrices, multisets, and tuples, the approach is generalizable to other solving paradigms and modeling languages beyond Essence.
Theoretical Foundation: The work serves as a theoretical background for future research, establishing a recursive semantics for type actions and group actions on compound structures.
Modesty on Performance: The authors acknowledge that complete symmetry breaking can be computationally expensive (prohibitively so in some cases) due to the sheer number of constraints required (linked to graph isomorphism complexity). Consequently, they emphasize the value of their framework in offering partial symmetry breaking options, allowing users to choose between solving speed and the completeness of symmetry elimination.

The paper concludes by identifying future work, including the investigation of representation-specific total orderings to improve efficiency and the exploration of symmetry breaking for non-symmetric permutation groups (e.g., chessboard symmetries).