1 Introduction↩︎

Optimization and automated reasoning, including constraint programming [1], [2], mixed-integer programming [3]–[5], satisfiability [6], [7], and satisfiability modulo theory [8], typically treat symmetries as redundant branches of the search tree to be pruned. A common way to address this redundancy is to add constraints which eliminate as many symmetric solutions as possible. These are the so-called symmetry breaking constraints which can be exploited, for example, in a static manner [8], [9], i.e., adding constraints a priori to restrict feasibility to orbit representatives.

In [10], we introduced an algebraic method for automatically generating symmetry-breaking constraints. Given the symmetry group of an integer linear program and a polynomial template \(h\), the method constructs breaker families of the form \(h(Px)-h(x)\le 0\). Unlike existing constructions, our method naturally yields both linear and nonlinear breakers and can be implemented with standard computer algebra tools. Experiments on bin-packing instances showed that quadratic breakers can outperform both linear variants and Gurobi’s [11] built-in symmetry handling.

These results raise a natural question: do the observed gains come from the breakers themselves, or from how a specific solver processes them? This is particularly important for quadratic breakers, since some solvers handle quadratic constraints natively, some reformulate them internally, and others require linear constraints, hence explicit linearization must be applied.

The goal of this paper is to study this solver dependence experimentally with different types of solvers: mathematical programming solvers such as Gurobi [11], CPLEX [12], and SCIP [13], the nonlinear and combinatorial optimization solver Hexaly [14], and the SMT solver Z3 [15].

We make three contributions:

Our experiments show that polynomial symmetry breaking is highly solver-sensitive. Compact quadratic breaker families (few variables, few permutations) often remain beneficial when handled natively, whereas reformulation or linearization may introduce variables and constraints that reduce or eliminate this advantage. Moreover, the same breaker family may improve performance for one solver and slow down another. Thus, automatically generated symmetry breakers should not be evaluated only by their mathematical strength or modelling convenience; their effectiveness must also be assessed together with the preprocessing and search mechanisms of the target solver.

2 Background: Polynomial Symmetry Breaking↩︎

This section gives an overview over the symmetry breaker generation which first appeared in [10].

We consider integer linear problems of the form \[\label{ILP} \text{minimize}\quad f(x), \qquad \text{subject to}\quad A x \geq b \quad\text{and}\quad x \in {U}^{n}\tag{1}\] where

We will call \(f\) the objective function of 1 . The set \(\{ x \in {\mathbb{R}}^{n} \colon A x \geq b \}\) will be refered to as the feasible set of 1 .

Solvers will typically explore the search space using tree-based methods such as branch-and-bound. Here, symmetries in the problem formulation can become problematic since the solver will repeatedly search essentially identical subtrees. Following [10], we identify symmetries with permutation matrices \(P\) where \(P\) maps the feasible set onto itself and fulfils \(f(P x) = f(x)\) for all \(x \in {U}^{n}\).

One possible strategy for avoiding the redundant searches that are caused by the presence of symmetries is to introduce additional constraints or (static) symmetry breakers to the problem. (See [10] for details.) While it is possible to add more than one symmetry breaker to a problem, one needs to take care that the breakers are compatible with each other (i. e., that the is at least one optimal solution which matches all the breakers).

In order to demonstrate the efficiency of the symmetry breakers generated through 1, [10] considered a variation of the bin-packing problem (see, e. g., [17] for more background on this problem). We will use the same example which we sketch out here briefly–see [10] for the details. The task is to place \(m\) items into as few bins as possible. For each \(k = 1, \ldots, m\), the \(k\)-th item has size \(s_k > 0\) and each bin can only contain items up to a total size of at most \(B > 0\). The problem can be modelled in the form of 1 via \[\label{BP} \begin{align} \text{minimize}\quad & y_1 + \ldots + y_n \\ \text{subject to}\quad & \forall k=1,\ldots,n\colon \textstyle\sum_{i=1}^m s_i x_{ik} \leq B y_k, \quad \forall i=1,\ldots,m\colon \textstyle\sum_{k=1}^n x_{ik} = 1, \\ & \forall i = 1,\ldots,m\; \forall k = 1,\ldots,n\colon x_{i,k} \in \{0,1\} \text{ and } y_k \in \{0,1\} \end{align}\tag{2}\] where \(y_k = 1\) means that the \(k\)-th bin is used and \(x_{ik} = 1\) means that the \(i\)-th item is to be placed into the \(k\)-th bin.

As in [10], we generate bin-packing instances with bin size \(B = 100\) and item sizes around \(B/2 = 50\). We consider four different classes: Class \(3\) has three different item sizes (\(49, 50, 51\)) and similarly classes \(5\), \(7\), and \(9\) have five, seven and nine different item sizes nearby \(B/2\).

Given an instance of 2 , we use 1 to generate a randomized family of symmetry breakers. For this, we need to know a set of the symmetries group for which we use [10]: Each symmetry consists of a permutation \(\pi\) of the \(i\)-indices in \(x_{ik}\) such that \(s_i = s_{\pi(i)}\) for all \(i\) which is combined with a permutation \(\psi\) of the \(k\)-indices in \(x_{ik}\) and \(y_k\). (In other words, \(x_{ik}\) maps to \(x_{\pi(i)\psi(k)}\) and \(y_k\) maps to \(y_{\psi(k)}\).)

For our experiments we started with a random polynomial \(h \in \mathbb{R}[x]\) which was generated from a set of fixed templates. These templates contained homogeneous polynomials of degrees \(1\) or \(2\) as well as inhomogeneous polynomials of degree \(2\) with a varying total number of variables. See 1 and ¿tbl:tab:perm-var-numbers? in 5 for more details. A full table with the exact parameters for each experiment is included in [16]. We then generated random permutation matrices \(P_1, \ldots, P_\ell\) where each permutation was obtained by composing a series of \(50\) random \(i\)- or \(k\)-transpositions. From this, we computed the symmetry breaker family \(H = \{ h(P_j x) - h(x) \colon j = 1, \ldots, \ell\}\) where for the quadratic templates we would additionally filter out any breakers \(h(P_j x) - h(x) \leq 0\) where \(\deg (h(P_j x) - h(x)) \leq 1\). (See the last column “Keep Only Degree 2” in 1.)

3 Experimental Results↩︎

We evaluate the performance of automatically generated polynomial symmetry-breaking constraints on randomly generated instances of near half-capacity bin-packing problems. For each benchmark instance, we first solve the original formulation to obtain a Baseline measurement, then generate families of random symmetry breakers using the method from 2 and compare the solver performance. All experiments were run on an Apple M2 Pro (10 cores).

3.1 Gurobi↩︎

Gurobi Optimizer [11] (academic license) was initially used in [10] to test the quadratic symmetry breakers in their original form. In that experiment, the breakers were passed directly to Gurobi’s nonconvex quadratic machinery and compared with the Baseline model and with Gurobi’s default settings. The main outcome was that quadratic breakers consistently outperform linear ones. Moreover, compact (i.e. few variables, few permutations) quadratic breakers, especially \(xy\) templates, were more reliable than linear breakers and often improved over Gurobi’s built-in symmetry handling. Larger breaker families (i.e. “many variables”, “numerous variables”) slow down the solver because the additional constraints could outweigh the reduction in symmetric search. The detailed experiment is reported in [10].

For this paper, we ran experiments with \(n \in \{99,100,700,900\}\). These values were chosen to align the Gurobi comparison with the range used in the CPLEX experiments (see 3.2)¹. We report these results separately for the four benchmark classes, because the behaviour differs substantially by class.

1 confirms once more the results from [10]. However, an exception is observed for class \(7\), where performance is generally worse than the Baseline. Since the Baseline is solved in only 0.08 work units, the potential benefit of additional symmetry breaking is limited, while the overhead introduced by the breakers may dominate.

Explicit linearization. For comparison with solvers and configurations that handle only linear models, we tested the following explicit linearization [18]: each product of two binary variables is replaced by an auxiliary binary variable. For instance, for binary variables \(x_1,x_2\), the product \(x_1x_2\) is represented by a new binary variable \(z_{12}\) and the constraints \[z_{12} - x_1 \leq 0, \qquad z_{12} - x_2 \leq 0, \qquad x_1 + x_2 - z_{12} \leq 1 . \label{eq:binary-product-linearization}\tag{3}\] For example, the quadratic inequality \(x_1x_2 + x_3 \leq 1\) is replaced by \(z_{12} + x_3 \leq 1\), together with constraints in 3 .

2 shows that linearization changes the performance profile of the breakers. Overall, the quadratic breakers in 1 perform better than their linearized version in 2. Linearization generally shows higher values and greater dispersion. For class \(7\) this is particularly obvious, but this is because the Baseline was already very fast. Moreover, the linearized quadratic breakers perform similar to the pure linear breakers.

3.2 CPLEX↩︎

CPLEX [12] was first tested on class \(3\) instances with \(n=900\), with both presolve and built-in symmetry handling disabled and with a deterministic time limit of \(4\,000\,000\) ticks. Under this configuration, linear symmetry breakers were faster than the Baseline. For quadratic symmetry breakers, CPLEX quickly reached solutions very close to optimality, but did not finish within the deterministic time limit. The solver logs indicated that CPLEX reformulated, or internally linearized, the quadratic constraints. Thus, in this setting, the solver was not necessarily solving the quadratic constraints exactly as written in the input model. We also disabled reductions which limited presolve reductions, but this did not provide a general mechanism for preserving arbitrary nonconvex quadratic constraints in their original form. The internal reformulation can produce strong relaxations that quickly reduce the optimality gap, but it may also leave the solver with a difficult final search near optimality. For this reason, the main CPLEX comparison uses only the explicit linearizations described above.

3 shows a different pattern from the Gurobi linearization in 2. For class \(3\), CPLEX is highly stable: almost all templates are below the Baseline and the spread is small. Classes \(5\) and \(9\) are much less stable. In both panels, several templates have large upper ranges or outliers, showing that the same linearized breakers can produce substantial slowdowns on other benchmark classes. Class \(7\) is mixed: the simpler templates are close to the Baseline or slightly below it, but \(y^2\) and larger combined templates can increase solver effort.

3.3 SCIP and Hexaly↩︎

We evaluated the SCIP Optimization Suite [13] under two solver configurations: the default configuration, using SCIP’s default presolve and symmetry-handling settings, and a second configuration in which both presolve and symmetry handling were disabled. For each configuration, we compared the Baseline formulation with the “few variables, few permutations, linearized \(x\)” variant. The results are reported in 2 in 5; for large \(n\), \(n \in \{700, 900\}\), neither configuration solved any instance within the \(1800\) seconds CPU-time limit. For the small \(n\), \(n \in \{99, 100\}\), the instances were solved, but the running-time effect of the symmetry breakers was not consistent.

We also considered Hexaly (academic license) [14], a solver for nonlinear and combinatorial optimization models. Unlike classical mixed-integer linear programming solvers, Hexaly represents models through expression graphs and can operate directly on nonlinear expressions, constraints, and objectives. Nevertheless, we did not investigate static symmetry-breaking constraints further in Hexaly; based on the available documentation and communication with the developers, such constraints may interact unfavorably with the solver’s internal search mechanisms, making their effect difficult to control or predict in this setting.

3.4 Z3↩︎

We tested Z3 optimization feature [19] on smaller instances, using \(n=99\) and class \(9\) (motivated by the CPLEX instance), with a CPU-time limit of 10 minutes. The Baseline optimization problem did not end within the time limit, nor the problems accompanied by symmetry breakers.

We further considered satisfiability-only problems obtained by dropping the objective function, in order to analyze the effect of the symmetry-breaking constraints.

4 and 5 summarize the satisfiability-only Z3 experiments with the tactic smt enabled. In this configuration, Z3 uses its standard SMT engine. The dashed line represents the Baseline. 4 confirms that the generated breakers can help Z3. However, the solved-time distributions must be interpreted together with the time-out counts, with \(x\) and \(x^2\) instances providing the best balance between robustness and runtime. 5 shows that breaker size is also important with the combination “handful” for permutations and “one” or “handful” for variables being the most efficient ones.

6 and 7 summarize the satisfiability-only Z3 experiments with the tactic smt disabled. In this configuration, the logs revealed that Z3 uses a pseudo-Boolean/bit-vector-backed engine. Note that the Baseline case did not finish in the allotted time, so it is not pictured in the figures. 7 suggests that the number of variables and permutations used in the quadratic symmetry breakers must be balanced carefully, with "handful", "handful" being the best combination. This indicates that effective symmetry breaking depends not only on the encoding template, but also on choosing a suitable breaker size.

4 Conclusions↩︎

We tested the method for automatically generating polynomial symmetry breakers [10] with mathematical programming solvers such as Gurobi [11], CPLEX [12], and SCIP [13], the non- linear and combinatorial optimization solver Hexaly [14], and the SMT solver Z3 [15].

The Gurobi results confirm the conclusions from [10] (see 3.1). The other solvers show more varied behavior. In particular, quadratic constraints are not supported as efficiently as in Gurobi. CPLEX preprocesses the quadratic inequalities, which negatively affects performance; linearizing the breakers using the method from [18] reduced the advantage of quadratic breakers over linear ones (see 3.1 and 3.2). Thus, quadratic breakers can currently be recommended only when the solver explicitly supports them.

Adding breakers, either quadratic or linear, can also worsen performance on instances that are already solved very quickly without them (see 3.1). This suggests generating quadratic breakers dynamically after a time threshold rather than adding them statically.

The number and size of breakers strongly affect performance, especially in the Z3 satisfiability-only experiments (see 3.4). Small variable sets (“one”, “handful”) and a smaller number of breakers (“handful”) avoided time-outs, while other categories had higher time-out rates. Interestingly, “many” permutations performed better than “few” permutations.

5 Appendix↩︎

We provide additional details for the breaker generation process. Similar to [10], breaker generation relies on templates which are governed by three parameters:

The different possible shapes are summarized in 1—they are exactly the same as the ones used in [10]. Note that each \(x\) in the shape column of 1 stands for a linear combination of several \(x_{ik}\) with different \(i \leq i, k \leq n\) rather than just for a single variable. Similarly, \(y\) denotes a linear combination of several \(y_k\) with different \(1 \leq k \leq n\). Moreover, the squared versions \(x^2\) and \(y^2\) do not mean taking the square of the same linear combinations but rather they symbolize the product of two different linear combinations of \(x_{ik}\) or \(y_k\), respectively. The “name of the template” column refers to the names of the breaker files generated by our program [16]. The “keep only degree \(2\)” column shows whether breakers of degree less than \(2\) should be discarded by the program (and thus not be included in the output). This is necessary since in the current implementation it is possible that the quadratic terms in \(h(P x)\) and \(h(x)\) cancel (e. g., if \(P\) only affects variables in the linear terms) leaving us with a linear breaker. However, because the purpose of our experiments is to test explicitly quadratic breakers, we have decided not to use any linear breaker which are created by this kind of accident.

The number of variables \(x_{ik}\) or \(y_k\) used for each linear combination depends on the number of bins \(n\) of the problem instance for which the breakers are to be generated. We provide an overview in [tbl:tab:var-numbers] where we explain the four different settings used in our templates. These are “one”, “handful”, “few”, “many”, and “numerous”. Note that the different shapes request different numbers of variables: generally, the quadratic terms (i. e., \(x^2\), \(y^2\), and \(x\,y\)) contain fewer distinct variables than the linear terms (i. e.\(x\) and \(y\)). Moreover, since there are \(n^2\) different \(x_{ik}\) but only \(n\) different \(y_k\), the terms containing \(y_k\) will usually have fewer variables. Thus, [tbl:tab:var-numbers] can only provide a range for the number of variables and not an exact value. See the source code quadratic-breakers.org in [16] for the precise numbers of variables used for each template.

Finally, there are three options for the number of permutations used for breaker generation which are shown in [tbl:tab:perm-numbers]. These correspond directly to \(\ell\) in 2. Note that not all permutations lead to useful breakers: in the current implementation it is possible that \(h(P x)\) and \(h(x)\) cancel each other leaving us with the true but useless inequality \(0 \leq 0\). The program will not output these trivial breakers. Moreover—as described above—, for the quadratic templates the program will skip all linear breakers generated accidentally. In addition, it is also possible that the same permutation (and hence the same breaker) is generated more than once. The current implementation will filter out duplicate breakers but not replace them by newly generated breakers. Thus, [tbl:tab:perm-numbers] gives only an upper bound of the number of breakers generated. However, we did find that due to the large number of possible permutations only very few trivial or duplicate breakers get generated. Thus, the actual number of breakers is usually very close the values in [tbl:tab:perm-numbers].

In 2, we report results obtained with SCIP. We used two options for running it: both presolve and symmetry disabled (column “Disabled”) and the “Default” SCIP setting. For lower \(n\), it is not obvious if the usage of symmetry breakers helps or not the solution process. It is easy to see that for high \(n\) the computations did not finish, hence we decided not to continue with further experiments.

This appendix reports additional Z3 satisfiability-only results, focusing on timeout behavior and runtime distributions under the two tactic configurations discussed in 3.4.

8 shows that the efficiency of the generated symmetry breakers is dependent on the template shape: all templates have both solved instances and time-outs with templates \(x\) and \(x^2\) giving the fewest time-outs. 10 shows that the solved instances are mostly concentrated between roughly \(200\) and \(350\) seconds.

Across the evaluated configurations, the \(x, y, x+y\) instances were consistently associated with the highest computational cost, with all such runs reaching timeout (see 9), hence they were not included in the subsequent figures. In contrast, the \(x^2\) and \(x^2+y\) templates exhibited the best and most robust performance, as also reflected in  6.

Finally,  11 shows that most benchmark instances that were solved finished relatively early, within the first 10 seconds, showing that overall the quadratic breakers are beneficial.

References↩︎