When Algebraic Symmetry Breaking Meets Solvers: An Experimental Study

Johannes Middeke; Madalina Erascu

arxiv: 2607.01726 · v1 · pith:JLT3WQ5Vnew · submitted 2026-07-02 · 💻 cs.SC

When Algebraic Symmetry Breaking Meets Solvers: An Experimental Study

Madalina Erascu , Johannes Middeke This is my paper

Pith reviewed 2026-07-03 02:15 UTC · model grok-4.3

classification 💻 cs.SC

keywords symmetry breakinginteger linear programmingpolynomial constraintsbin-packingsolver performancemathematical programmingSMT solversexperimental evaluation

0 comments

The pith

Polynomial symmetry breaking for integer linear programs works differently depending on the solver used.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper evaluates automatically generated polynomial symmetry breaking constraints added to integer linear programs. It compares three ways of handling those constraints—native quadratic support, solver reformulation, and explicit linearization—on near half-capacity bin-packing instances. Experiments across several mathematical programming solvers and SMT solvers reveal that performance changes are strongly tied to the particular solver and handling method. Compact quadratic breaker families sometimes speed up solving, while larger sets or linearization often increase model size and slow search. The study therefore concludes that symmetry breakers cannot be treated as universal, solver-independent additions.

Core claim

Experiments with several mathematical programming solvers and satisfiability modulo theory solvers show that the effectiveness of polynomial symmetry breaking is strongly solver-dependent. Compact quadratic breaker families can improve performance, whereas linearization, large breaker sets, or solver reformulations may offset these gains through increased model size or less favorable search behavior. These results suggest that automatically generated symmetry breakers should be evaluated in a solver-aware manner rather than treated as solver-independent additions to a model.

What carries the argument

Automatically generated polynomial symmetry breaking constraints, compared through solver-native quadratic handling, internal reformulation, and explicit linearization.

If this is right

Compact quadratic breaker families improve performance on the tested bin-packing benchmarks for some solvers.
Explicit linearization of the breakers increases model size and can cancel out any speed gains.
Large breaker families produce less favorable search behavior in the solvers examined.
Solver-internal reformulation of quadratic constraints can reduce the benefit of adding symmetry breakers.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Generator tools for symmetry breakers could be extended to take solver type and native capabilities as input parameters.
The same experimental protocol could be applied to other problem families such as scheduling or graph problems to test whether the solver dependence persists.
Solver portfolios that route instances to the solver best matched to a given breaker family might exploit the observed variation.

Load-bearing premise

The near half-capacity bin-packing benchmarks sufficiently represent how symmetry breaking behaves in general integer linear programs.

What would settle it

A set of experiments on a wider collection of integer linear programs and additional solvers that shows consistent gains from polynomial symmetry breaking regardless of handling method would falsify the solver-dependence claim.

Figures

Figures reproduced from arXiv: 2607.01726 by Johannes Middeke, Madalina Erascu.

**Figure 2.** Figure 2: Gurobi relative performance of the tested symmetry-breaking variants (liniarized). [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** Figure 3: CPLEX relative performance of the tested symmetry-breaking variants (liniarized). [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗

**Figure 4.** Figure 4: Timings for the Z3 experiments (tactic smt enabled) grouped by the template shape. The times are shown in seconds. The graph considers only the instances which did finish within the time bound of 10 min. Time-Outs 2 99 67 Baseline 200 300 400 500 600 handful few many (a) Time per number of permutations. Time-Outs 0 2 105 61 Baseline 200 300 400 500 600 one handful few many (b) Time per number of variable… view at source ↗

**Figure 5.** Figure 5: Timings for Z3 experiments (tactic smt enabled) grouped by number of variables or number of permutations. The times are shown in seconds. The graph considers only the instances which did finish within the time bound of 10 min. Time-Outs 0 16 7 11 11 0 0 100 200 300 x 2 y 2 x y x 2 + y 2 x + y 2 x 2 + y [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗

**Figure 6.** Figure 6: Timings for the Z3 experiments (tactic smt disabled) grouped by the template shape. The times are shown in seconds. The graph considers only the instances which did finish within the time bound of 6 min. 7 [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗

**Figure 7.** Figure 7: Timings for Z3 experiments (tactic smt disabled) grouped by number of variables or number of permutations. The times are shown in seconds. The graph considers only the instances which did finish within the time bound of 6 min. The Gurobi results confirm the conclusions from [7] (see Subsection 3.1). The other solvers show more varied behavior. In particular, quadratic constraints are not supported as effic… view at source ↗

**Figure 8.** Figure 8: Number of time-outs for the Z3 (tactic smt enabled) experiments by template shape. The graph shows how many instances for each shape did not finish within in the time bound of 10 min compared to the number of instances which did finish. 0 10 20 30 40 50 x y x + y x 2 y 2 x y x 2 + y 2 x + y 2 x 2 + y Time-Out yes no [PITH_FULL_IMAGE:figures/full_fig_p012_8.png] view at source ↗

**Figure 9.** Figure 9: Number of time-outs for the Z3 (tactic smt disabled) experiments by template shape. The graph shows how many instances for each shape did not finish within in the time bound of 6 min compared to the number of instances which did finish. 12 [PITH_FULL_IMAGE:figures/full_fig_p012_9.png] view at source ↗

**Figure 10.** Figure 10: Z3 (tactic smt enabled) count of how many instances finished within which time interval. The intervals have a width of 10 s starting at 0 s. The graph shows only the instances which finished within the time bound of 10 min. In addition there were 168 time-outs. 0 50 100 150 200 0 100 200 300 [PITH_FULL_IMAGE:figures/full_fig_p013_10.png] view at source ↗

**Figure 11.** Figure 11: Z3 (tactic smt disabled) count of how many instances finished within which time interval. The intervals have a width of 10 s starting at 0 s. The graph shows only the instances which finished within the time bound of 6 min. In addition there were 37 time-outs. 13 [PITH_FULL_IMAGE:figures/full_fig_p013_11.png] view at source ↗

read the original abstract

We present an experimental evaluation of automatically generated polynomial symmetry breaking constraints for integer linear programs. Starting from the method that we introduced at the International Symposium on Symbolic and Algebraic Computation (ISSAC) 2026, we compare solver native quadratic handling, solver-internal reformulation, and explicit linearization on near half-capacity bin-packing benchmarks. Experiments with several mathematical programming solvers and satisfiability modulo theory solvers show that the effectiveness of polynomial symmetry breaking is strongly solver-dependent. Compact quadratic breaker families can improve performance, whereas linearization, large breaker sets, or solver reformulations may offset these gains through increased model size or less favorable search behavior. These results suggest that automatically generated symmetry breakers should be evaluated in a solver-aware manner rather than treated as solver-independent additions to a model.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The experiments show solver-dependent effects from polynomial symmetry breakers on these bin-packing cases, but the single benchmark family leaves the general recommendation on shaky ground.

read the letter

This paper runs their ISSAC 2026 polynomial symmetry breaking method on near half-capacity bin-packing instances and compares how different solvers handle the resulting quadratic constraints versus linearized or reformulated versions. The main finding is that compact quadratic breakers sometimes improve runtimes while larger sets or explicit linearization often erase the benefit through model size or search changes. That difference appears across the tested MP and SMT solvers.

The work is new as an empirical follow-up. It supplies concrete performance numbers that were not in the earlier paper and makes a practical observation about not treating breakers as solver-independent add-ons.

The soft spot is the benchmark choice. All instances come from one narrow class where symmetries are just permutations of identical items and the capacity is near half. That structure may interact with solvers in ways that do not appear in other ILPs with cyclic, graph, or subset symmetries. The claim that breakers should be evaluated solver-aware therefore rests on limited evidence; the stress-test concern holds up.

The experimental design itself looks reasonable on the surface, with no obvious circularity or invented entities. Citations are mostly to their own prior work and standard solver literature.

This is for people who already work on algebraic symmetry methods inside optimization solvers. A reader who needs data on how quadratic handling plays out across tools will find something usable here. It is not a foundational result but adds a data point worth checking.

I would send it to peer review so the experimental details and statistical support can be examined directly.

Referee Report

1 major / 1 minor

Summary. The paper reports an experimental evaluation of automatically generated polynomial symmetry breaking constraints for integer linear programs. Building on a prior ISSAC 2026 method, it compares solver-native quadratic handling, solver-internal reformulation, and explicit linearization on near half-capacity bin-packing benchmarks. Experiments across mathematical programming and SMT solvers indicate that the effectiveness of these breakers is strongly solver-dependent, with compact quadratic families sometimes improving performance while linearization or large sets can degrade it due to model size or search behavior. The authors conclude that such breakers should be evaluated in a solver-aware manner.

Significance. If the reported solver dependence holds beyond the tested instances, the work would usefully highlight that algebraic symmetry-breaking techniques cannot be treated as solver-independent additions to models. This could shift evaluation practices in the intersection of symbolic computation and optimization solvers, encouraging more targeted integration of polynomial breakers. The experimental framing provides concrete data on quadratic vs. linearized handling, which is a practical contribution even if limited in scope.

major comments (1)

[Abstract] Abstract and benchmark description: All experiments use only near half-capacity bin-packing instances whose symmetries are limited to permutations of identical items under capacity-induced tightness. This narrow symmetry structure and problem class may interact with solvers in ways not representative of other ILP families (e.g., those with cyclic, graph-automorphism, or variable-subset symmetries). Because the central claim of strong solver dependence and the recommendation for solver-aware evaluation rest on these results, the restriction is load-bearing and requires either additional benchmark families or explicit qualification of the scope.

minor comments (1)

[Abstract] The abstract mentions 'several' solvers and 'statistical analysis' implicitly through performance claims, but lacks explicit details on the number of instances, run-time cutoffs, or variance reporting; adding these would improve verifiability without altering the core findings.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive comment on the scope of our benchmarks. We address it below by agreeing to add explicit qualifications rather than expanding the experimental suite.

read point-by-point responses

Referee: [Abstract] Abstract and benchmark description: All experiments use only near half-capacity bin-packing instances whose symmetries are limited to permutations of identical items under capacity-induced tightness. This narrow symmetry structure and problem class may interact with solvers in ways not representative of other ILP families (e.g., those with cyclic, graph-automorphism, or variable-subset symmetries). Because the central claim of strong solver dependence and the recommendation for solver-aware evaluation rest on these results, the restriction is load-bearing and requires either additional benchmark families or explicit qualification of the scope.

Authors: We agree that the experiments are restricted to permutation symmetries of identical items in near half-capacity bin-packing instances. This class was selected because it produces well-defined, automatically detectable symmetries that the ISSAC 2026 generation method targets, enabling a controlled comparison of quadratic handling, reformulation, and linearization across solvers. While we believe permutation symmetries are representative of a practically relevant subclass of ILP symmetries, we acknowledge that cyclic, graph-automorphism, or other structures could interact differently with solvers. In the revised version we will add explicit scope qualifications to the abstract, introduction, and conclusions, stating that the reported solver dependence is demonstrated for this symmetry class and problem family, and that extending the evaluation to additional ILP families remains valuable future work. We do not introduce new benchmark families, as that would require substantial new symmetry-generation experiments outside the current study. revision: yes

Circularity Check

0 steps flagged

No circularity: experimental evaluation stands on its own data

full rationale

The paper is an empirical study that applies a previously published symmetry-breaking method (cited from ISSAC 2026) to a fixed benchmark family and measures solver performance. The central claim—that effectiveness is strongly solver-dependent—is obtained directly from the reported runtimes and is not derived from any equation, fitted parameter, or self-citation that reduces to the input data by construction. No self-definitional steps, renamed predictions, or load-bearing uniqueness theorems appear in the derivation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper is an experimental study and does not introduce new mathematical axioms or parameters beyond standard ones in the field.

axioms (1)

domain assumption Standard assumptions of integer linear programming and solver behavior
The paper relies on typical modeling assumptions in optimization.

pith-pipeline@v0.9.1-grok · 5655 in / 1068 out tokens · 42852 ms · 2026-07-03T02:15:46.734609+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

19 extracted references · 4 canonical work pages · 1 internal anchor

[1]

Aloul, Igor L

Fadi A. Aloul, Igor L. Markov, and Karem A. Sakallah. Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability. InProceedings of the 40th Design Automation Conference (DAC), pages 836–839. ACM, 2003

2003
[2]

Egon Balas. Extension de l’Algorithme Additif ` a la Programmation en Nombres Entiers et ` a la Programmation Non Lin´ eaire.Comptes Rendus Hebdomadaires des Sceances de l’Academie des Sciences, 258(21):5136, 1964

1964
[3]

In Christel Baier and Cesare Tinelli, editors,Tools and Algorithms for the Construction and Analysis of Systems, pages 194–199, Berlin, Heidelberg, 2015

Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein.νZ - An Optimizing SMT Solver. In Christel Baier and Cesare Tinelli, editors,Tools and Algorithms for the Construction and Analysis of Systems, pages 194–199, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg

2015
[4]

Crawford, Matthew L

James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy. Symmetry- Breaking Predicates for Search Problems. InProceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR’96), pages 148–159. Morgan Kauf- mann, 1996

1996
[5]

Z3: An Efficient SMT Solver

Leonardo De Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. InInternational conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008. 8 When Algebraic Symmetry Breaking Meets Solvers: An Experimental Study Era¸ scu, Middeke

2008
[6]

Advances in Symmetry Break- ing for SAT Modulo Theories.arXiv preprint arXiv:1908.00860, 2019

Saket Dingliwal, Ronak Agarwal, Happy Mittal, and Parag Singla. Advances in Symmetry Break- ing for SAT Modulo Theories.arXiv preprint arXiv:1908.00860, 2019

work page arXiv 1908
[7]

Automatic Generation of Polynomial Symmetry Break- ing Constraints

M˘ ad˘ alina Era¸ scu and Johannes Middeke. Automatic Generation of Polynomial Symmetry Break- ing Constraints. https://arxiv.org/abs/2602.08297, 2026

work page arXiv 2026
[8]

Polynomial Symmetry Breakers.https://github.com/ merascu/PolynomialSymmetryBreakers, 2026

M˘ ad˘ alina Era¸ scu and Johannes Middeke. Polynomial Symmetry Breakers.https://github.com/ merascu/PolynomialSymmetryBreakers, 2026

2026
[9]

Gent, Karen E

Ian P. Gent, Karen E. Petrie, and Jean-Fran¸ cois Puget. Symmetry in Constraint Programming. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors,Handbook of Constraint Programming, pages 329–376. Elsevier, 2006

2006
[10]

Gurobi Optimizer Reference Manual.https://www.gurobi.com, 2024

Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual.https://www.gurobi.com, 2024

2024
[11]

Hexaly Optimizer.https://www.hexaly.com, 2026

Hexaly. Hexaly Optimizer.https://www.hexaly.com, 2026

2026
[12]

The SCIP Opti- mization Suite 10.0.arXiv preprint arXiv:2511.18580, 2025

Christopher Hojny, Mathieu Besan¸ con, Ksenia Bestuzheva, Sander Borst, Jo˜ ao Dion´ ısio, Johannes Ehls, Leon Eifler, Mohammed Ghannam, Ambros Gleixner, Adrian G¨ oß, et al. The SCIP Opti- mization Suite 10.0.arXiv preprint arXiv:2511.18580, 2025

work page arXiv 2025
[13]

Packing and Partitioning Orbitopes.Mathematical Programming, 114(1):1–36, 2008

Volker Kaibel and Marc Pfetsch. Packing and Partitioning Orbitopes.Mathematical Programming, 114(1):1–36, 2008

2008
[14]

IBM ILOG CPLEX Optimization Studio.Version, 12(1987-2018):1, 1987

CPLEX User’s Manual. IBM ILOG CPLEX Optimization Studio.Version, 12(1987-2018):1, 1987

1987
[15]

Pruning by Isomorphism in Branch-and-Cut.Mathematical Programming, 94(1):71–90, 2002

Fran¸ cois Margot. Pruning by Isomorphism in Branch-and-Cut.Mathematical Programming, 94(1):71–90, 2002

2002
[16]

John Wiley & Sons, Inc., 1990

Silvano Martello and Paolo Toth.Knapsack Problems: Algorithms and Computer Implementations. John Wiley & Sons, Inc., 1990

1990
[17]

On the Satisfiability of Symmetrical Constrained Satisfaction Problems

Jean-Francois Puget. On the Satisfiability of Symmetrical Constrained Satisfaction Problems. In International Symposium on Methodologies for Intelligent Systems, pages 350–361. Springer, 1993

1993
[18]

Symmetry Breaking Inequalities from the Schreier-Sims Table

Domenico Salvagnin. Symmetry Breaking Inequalities from the Schreier-Sims Table. InInter- national Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 521–529. Springer, 2018

2018
[19]

Symmetry Breaking Constraints: Recent Results

Toby Walsh. Symmetry Breaking Constraints: Recent Results.arXiv preprint arXiv:1204.3348, 2012. A Appendix We provide additional details for the breaker generation process. Similar to [7], breaker gen- eration relies on templates which are governed by three parameters: the shape of the base polynomialh, the number of variables in the base polynomialh, and...

work page internal anchor Pith review Pith/arXiv arXiv 2012

[1] [1]

Aloul, Igor L

Fadi A. Aloul, Igor L. Markov, and Karem A. Sakallah. Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability. InProceedings of the 40th Design Automation Conference (DAC), pages 836–839. ACM, 2003

2003

[2] [2]

Egon Balas. Extension de l’Algorithme Additif ` a la Programmation en Nombres Entiers et ` a la Programmation Non Lin´ eaire.Comptes Rendus Hebdomadaires des Sceances de l’Academie des Sciences, 258(21):5136, 1964

1964

[3] [3]

In Christel Baier and Cesare Tinelli, editors,Tools and Algorithms for the Construction and Analysis of Systems, pages 194–199, Berlin, Heidelberg, 2015

Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein.νZ - An Optimizing SMT Solver. In Christel Baier and Cesare Tinelli, editors,Tools and Algorithms for the Construction and Analysis of Systems, pages 194–199, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg

2015

[4] [4]

Crawford, Matthew L

James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy. Symmetry- Breaking Predicates for Search Problems. InProceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR’96), pages 148–159. Morgan Kauf- mann, 1996

1996

[5] [5]

Z3: An Efficient SMT Solver

Leonardo De Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. InInternational conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008. 8 When Algebraic Symmetry Breaking Meets Solvers: An Experimental Study Era¸ scu, Middeke

2008

[6] [6]

Advances in Symmetry Break- ing for SAT Modulo Theories.arXiv preprint arXiv:1908.00860, 2019

Saket Dingliwal, Ronak Agarwal, Happy Mittal, and Parag Singla. Advances in Symmetry Break- ing for SAT Modulo Theories.arXiv preprint arXiv:1908.00860, 2019

work page arXiv 1908

[7] [7]

Automatic Generation of Polynomial Symmetry Break- ing Constraints

M˘ ad˘ alina Era¸ scu and Johannes Middeke. Automatic Generation of Polynomial Symmetry Break- ing Constraints. https://arxiv.org/abs/2602.08297, 2026

work page arXiv 2026

[8] [8]

Polynomial Symmetry Breakers.https://github.com/ merascu/PolynomialSymmetryBreakers, 2026

M˘ ad˘ alina Era¸ scu and Johannes Middeke. Polynomial Symmetry Breakers.https://github.com/ merascu/PolynomialSymmetryBreakers, 2026

2026

[9] [9]

Gent, Karen E

Ian P. Gent, Karen E. Petrie, and Jean-Fran¸ cois Puget. Symmetry in Constraint Programming. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors,Handbook of Constraint Programming, pages 329–376. Elsevier, 2006

2006

[10] [10]

Gurobi Optimizer Reference Manual.https://www.gurobi.com, 2024

Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual.https://www.gurobi.com, 2024

2024

[11] [11]

Hexaly Optimizer.https://www.hexaly.com, 2026

Hexaly. Hexaly Optimizer.https://www.hexaly.com, 2026

2026

[12] [12]

The SCIP Opti- mization Suite 10.0.arXiv preprint arXiv:2511.18580, 2025

Christopher Hojny, Mathieu Besan¸ con, Ksenia Bestuzheva, Sander Borst, Jo˜ ao Dion´ ısio, Johannes Ehls, Leon Eifler, Mohammed Ghannam, Ambros Gleixner, Adrian G¨ oß, et al. The SCIP Opti- mization Suite 10.0.arXiv preprint arXiv:2511.18580, 2025

work page arXiv 2025

[13] [13]

Packing and Partitioning Orbitopes.Mathematical Programming, 114(1):1–36, 2008

Volker Kaibel and Marc Pfetsch. Packing and Partitioning Orbitopes.Mathematical Programming, 114(1):1–36, 2008

2008

[14] [14]

IBM ILOG CPLEX Optimization Studio.Version, 12(1987-2018):1, 1987

CPLEX User’s Manual. IBM ILOG CPLEX Optimization Studio.Version, 12(1987-2018):1, 1987

1987

[15] [15]

Pruning by Isomorphism in Branch-and-Cut.Mathematical Programming, 94(1):71–90, 2002

Fran¸ cois Margot. Pruning by Isomorphism in Branch-and-Cut.Mathematical Programming, 94(1):71–90, 2002

2002

[16] [16]

John Wiley & Sons, Inc., 1990

Silvano Martello and Paolo Toth.Knapsack Problems: Algorithms and Computer Implementations. John Wiley & Sons, Inc., 1990

1990

[17] [17]

On the Satisfiability of Symmetrical Constrained Satisfaction Problems

Jean-Francois Puget. On the Satisfiability of Symmetrical Constrained Satisfaction Problems. In International Symposium on Methodologies for Intelligent Systems, pages 350–361. Springer, 1993

1993

[18] [18]

Symmetry Breaking Inequalities from the Schreier-Sims Table

Domenico Salvagnin. Symmetry Breaking Inequalities from the Schreier-Sims Table. InInter- national Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 521–529. Springer, 2018

2018

[19] [19]

Symmetry Breaking Constraints: Recent Results

Toby Walsh. Symmetry Breaking Constraints: Recent Results.arXiv preprint arXiv:1204.3348, 2012. A Appendix We provide additional details for the breaker generation process. Similar to [7], breaker gen- eration relies on templates which are governed by three parameters: the shape of the base polynomialh, the number of variables in the base polynomialh, and...

work page internal anchor Pith review Pith/arXiv arXiv 2012