REVIEW 1 major objections 1 minor 19 references
When Algebraic Symmetry Breaking Meets Solvers: An Experimental Study
T0 review · 1 major / 1 minor · reviewed 2026-07-03 · grok-4.3
Pith's one-line read Polynomial symmetry breaking for integer linear programs works differently depending on the solver used.
desk verdict 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 →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
Automatically generated polynomial symmetry breaking constraints, compared through solver-native quadratic handling, internal reformulation, and explicit linearization.
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.
Extended reading notes
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.
Load-bearing premise
The near half-capacity bin-packing benchmarks sufficiently represent how symmetry breaking behaves in general integer linear programs.
Editorial extensions
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.
Reading between the lines
- 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.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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
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
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.
Assumptions & free parameters
assumptions (1)
- domain assumption Standard assumptions of integer linear programming and solver behavior
Cite this review
Pith. "Pith review of When Algebraic Symmetry Breaking Meets Solvers: An Experimental Study." pith.science (2026). https://pith.science/paper/JLT3WQ5V
@misc{pith2026260701726,
author = {Pith},
title = {Pith review of: When Algebraic Symmetry Breaking Meets Solvers: An Experimental Study},
year = {2026},
howpublished = {\url{https://pith.science/paper/JLT3WQ5V}},
note = {Machine review of arXiv:2607.01726}
}
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.
Figures
Figures from the paper (8 more)
Reference graph
Works this paper leans on
-
[1]
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
work page 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
work page 1964
-
[3]
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
work page 2015
-
[4]
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
work page 1996
-
[5]
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
work page 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
-
[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
-
[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
work page 2026
Show all 19 references
-
[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
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]
name of the template
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 sha...
2012 arXiv
Reviewed July 3, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.