Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets

A literal $\mathrm{\ell }$ is a Boolean variable $x$ or its negation $\overline{x}=1-x$, where variables take values $0$ (false) or $1$ (true). A pseudo-Boolean (PB) constraint $C$ is a $0$–$1$ linear inequality ${\sum }_i{a}_i{\mathrm{\ell }}_i\ge A$, where $a_i$ and $A$ are integers. Without loss of generality, we often assume PB constraints to be in normal form, meaning that the literals ${\mathrm{\ell }}_i$ are over distinct variables, each coefficient $a_i$ is positive and the degree (of falsity) $A$ is non-negative. A pseudo-Boolean formula $F$ is a conjunction ${\bigwedge }_j{C}_j$ of PB constraints. When convenient, we view $F$ as a set of constraints. For a constraint $C$, $\text{lit}(C)$ is the set of literals that appear in $C$. For a pseudo-Boolean formula $F$, $\text{lit}(F)={\bigcup }_{C\in F}\text{lit}(C)$. An objective $O$ is an expression ${\sum }_i{w}_i{\mathrm{\ell }}_i+lb$ where the coefficients $w_i$ and the constant $lb$ are integers ($lb$ stands for “lower bound”: when the $w_i$ are all possible, this constant term is indeed a lower bound on the cost).

A substitution (sometimes also called a witness) $\omega$ is a mapping of variables to $0$, $1$ and literals. An assignment $\alpha$ is a substitution that maps each variable in its domain into $\{0,1\}$. An assignment is complete for $F$ if it assigns a value to each variable of interest (where the set of variables should be clear from the context). We write $\omega (C)$ for the constraint obtained from $C$ by replacing each variable $x$ in the domain of $\omega$ by $\omega (x)$ (and implicitly normalizing); $\omega (O)$, $\omega (\mathrm{\ell })$, $\omega (F)$ are defined analogously.

A (normalized) PB constraint $C={\sum }_i{a}_i{\mathrm{\ell }}_i\ge A$ is trivial if $A\le 0$ and contradictory if . The constraint $C$ is satisfied by $\alpha$ (denoted $\alpha \vDash C$) if $\alpha (C)$ is trivial. A PB formula is satisfied if all of its constraints are satisfied. An instance of the pseudo-Boolean optimization problem is a tuple $(F,O)$ with $F$ a PB formula and $O$ an objective to minimize. A complete assignment $\alpha$ is a solution of $(F,O)$ if $\alpha \vDash F$ and is optimal if also $\alpha (O)\le \beta (O)$ for each solution $\beta$ of $(F,O)$. The optimal cost of $(F,O)$ is $\alpha (O)$ for an optimal solution of $(F,O)$.

Following [37], a constraint $C$ is an unsatisfiable core of $(F,O)$ if the following conditions hold: (i) the literals in $C$ are objective literals or their negations and (ii) all assignments $\alpha$ that satisfy $F$ also satisfy $C$ (denoted by $F\vDash C$). In other words, an unsatisfiable core is an implied constraint that only mentions objective literals.

The following proposition forms the basis for how the IHS approach to PBO uses cores to compute optimal solutions.

In words, Proposition 2 states that the cost of the optimal (minimum-cost) solutions to any set of cores is a lower bound on the optimal cost of the instance.

A substitution $\sigma$ is called a (syntactic) weak symmetry of $(F,O)$ if $\sigma (F)=F$. If $\sigma (O)=O$ further holds, $\sigma$ is a (strong) symmetry. For strong symmetries, $\alpha$ is an optimal solution of $(F,O)$ if and only if $\alpha \circ \sigma$ is an optimal solution of $(F,O)$. We also consider a subset of weak symmetries that we call core-preserving symmetries. A weak symmetry $\sigma$ is core-preserving if $\sigma (\mathrm{\ell })$ is an objective literal if and only if $\mathrm{\ell }$ is. Similarly to weak symmetries, and in contrast to strong ones, a core-preserving symmetry $\sigma$ is not guaranteed to preserve the cost of solutions, i.e., $\alpha (O)$ need not equal $\alpha \circ \sigma (O)$. In contrast to weak symmetries, however, core-preserving symmetries are guaranteed to map cores to cores, i.e., $\sigma (C)$ is a core of $(F,O)$ if and only if $C$ is. If $\mathrm{\Sigma }$ is a set of symmetries, we write $⟨\mathrm{\Sigma }⟩$ for the group generated by $\mathrm{\Sigma }$. If $\mathrm{\Sigma }$ is a set of symmetries acting on a set $S$ (e.g., acting on the set of cores as just defined), the orbit of $s\in S$ under $\mathrm{\Sigma }$, denoted $𝒪(s,\mathrm{\Sigma })$, is the set $\{\sigma (s)\mid \sigma \in ⟨\mathrm{\Sigma }⟩\}$.

When symmetries are present, they can slow down search of a PBO solver, causing the solver to explore many symmetric subareas of the search space of solutions. One way to deal with symmetric search spaces is to add symmetry-breaking constraints. Specifically, given a (strong) symmetry $\sigma$, a common approach is to add a (set of) constraint(s) that is satisfied by an assignment $\alpha$ if and only if $\alpha$ is lexicographically smaller than (or equal to) $\alpha \circ \sigma$ [1]. This can be achieved with a single pseudo-Boolean constraint $L{L}_{\sigma }$ (called a lex-leader constraint) of the form

or by expressing the constraint as a set of constraints with smaller coefficients using auxiliary variables (see for instance [19]). Since weak symmetries do not preserve the costs of solutions, lex-leader constraints over a weak symmetry might change the optimal cost of a PBO instance. Van Caudenberg and Bogaerts [40] generalized the lex-leader constraint to weak symmetries, which then becomes a dominance constraint

which states that the objective value must be smaller than or equal to the objective of the symmetric assignment, and, furthermore, if the objective values are equal, the assignment must be lexicographically smaller than its symmetric counterpart.

An alternative to defining symmetries as substitutions is to define symmetries as permutations of literals respecting negation, i.e., via a permutation $\pi$ of the literals such that $\pi (\overline{x})=\overline{\pi }(x)$ for each $x$. We will use disjoint cycle notation and write, for instance, $(x\overline{y}z)$ (or $(x\overline{y}z)(\overline{x}y\overline{z})$ if we also want to spell out the redundant information) for the symmetry that maps $x$ to $\overline{y}$, $\overline{y}$ to $z$ and $z$ to $x$ and all other variables to themselves.

In practice, there can be exponentially many symmetries and hence breaking all of them, e.g., via lex-leader constraints, is in general infeasible. The most common way of dealing with this is to simply break a set of generators of the symmetry group, without formal guarantees on completeness, i.e., on that all symmetries would be broken. A set of generators is typically detected via a graph representing a simplification of the syntax tree of the formula and computing automorphisms of this graph [2]. Some tools go further then detecting an arbitrary set of generators, aiming to identify structure in the symmetry group [19, 4, 3]. As an example, these tools aim to detect row interchangeability [17], representing a symmetry as a matrix $M$ of literals such that each two rows of the matrix are interchangeable in the sense that ${\sigma }_{ij}$ maps every literal $M_{ik}$ to $M_{jk}$, each $M_{jk}$ to $M_{ik}$, and other literals to themselves. If one uses the “right” set of generators, and the “right” order of the variables at hand, the entire group generated by such a matrix can be broken with a polynomially-sized set of symmetry breaking constraints.

Algorithm 1 details PBO-IHS, the implicit hitting set algorithm for pseudo-Boolean optimization [37, 38]. The highlighted lines correspond to the symmetric core learning extension we detail in Section 3 and should be ignored in this section.

Given a PBO instance $(F,O)$, PBO-IHS begins by checking the existence of solutions of $(F,O)$ by invoking PB decision procedure PB-Solve on $F$ (Line 2). The call returns an indicator sat? for satisfiability and a solution ${\alpha }_{\mathrm{𝑏𝑒𝑠𝑡}}$ in the positive case. Given ${\alpha }_{\mathrm{𝑏𝑒𝑠𝑡}}$, an upper bound $ub$ and a lower bound $lb$ on the optimal cost of the instance are initialized to ${\alpha }_{\mathrm{𝑏𝑒𝑠𝑡}}(O)$ and $-\mathrm{\infty }$, respectively, on line 5. During the search, ${\alpha }_{\mathrm{𝑏𝑒𝑠𝑡}}$ will always contain the currently best-known solution for which ${\alpha }_{\mathrm{𝑏𝑒𝑠𝑡}}(O)=ub$. A set $𝒦$ of cores of the instance is initialized to $\mathrm{\varnothing }$ and the main search loop (lines 7-15) entered. The main search loop iterates until $lb=ub$, at which point ${\alpha }_{\mathrm{𝑏𝑒𝑠𝑡}}$ is known to be optimal. Each iteration begins with the computation of an optimal solution $\gamma$ of the instance $(𝒦,O)$ consisting of the cores found so far and the objective (Line 9). In practice, $\gamma$ is computed by solving the hitting set IP in Figure 1 with an integer programming (IP) solver. By Proposition 2, $\gamma (O)$ will be a lower bound on the optimal cost of the instance. Since no cores are ever removed from $𝒦$, the values of $\gamma (O)$ will be non-decreasing over the iterations, so $lb$ can always be updated on Line 9. If the algorithm does not terminate on Line 10, the procedure Extract-Core next computes a new core $C$ of $(F,O)$ not satisfied by $\gamma$. This is achieved by invoking a decision procedure for PB constraints of $F$ under the assumptions $\gamma$. The result of this call will either be a solution that extends $\gamma$, or a constraint $C$ (learned using standard conflict analysis) falsified by $\gamma$ but for which $F\vDash C$.

Each extracted core in IHS witnesses that the current $\gamma$ cannot be extended to an optimal solution of the original instance. As a byproduct, Extract-Core also often obtains a solution ${\alpha }^{\prime }$ of cost ${\alpha }^{\prime }(O)=u{b}^{\prime }$, which it also returns. The cost of ${\alpha }^{\prime }$ can (but need not) be lower than the current upper bound; hence, termination is checked on Line 13. If the algorithm does not terminate, the new core is added to $𝒦$, and IHS reiterates.

SCL is based on the observation that given a PBO instance $(F,O)$, a core $C$, and a core-preserving symmetry $\sigma$, the constraint $\sigma (C)$ obtained by applying $\sigma$ to $C$ is also a core of $(F,O)$. Symmetric core learning uses core-preserving symmetries of a PBO instance to generate new cores dynamically during search, with the key aims of decreasing the number of calls to the Extract-Core and Min-Sol procedures of PBO-IHS, while at the same time avoiding the generation of (a potentially large number) of lex-leader constraints before search.

The IHS approach to PBO extended with symmetric core learning is obtained by including the highlighted lines of Algorithm 1. During the initialization phase, the algorithm computes a set of core-preserving symmetries of the PBO instance to be solved on Line 6. The symmetries are used during each iteration of the search loop by the SCL procedure on Line 14 to generate a set $K$ of cores that are symmetric to the core $C$ computed by Extract-Core, with the aim of increasing the number of cores added to $𝒦$ in each iteration of IHS search.

An intuition underlying symmetric core learning is that if we have a symmetry $\sigma$ and a core $C$, then computing a symmetric core $\sigma (C)$ is very fast. In contrast, extracting cores with the subroutine Extract-Core invokes a decision procedure for an NP-hard constraint language, which could require a significant amount of time. Furthermore, in theory, a single symmetry can be used to generate many different symmetric cores. Thus, we expect symmetric core learning to be efficient for solving instances where the time required to compute core-preserving symmetries and invoking SCL is lower than the time needed to extract enough cores to terminate using only Extract-Core.

We detail two variants of symmetric core learning, i.e., instantiations of the SCL procedure of Algorithm 1. In explicit symmetric core learning, detailed in Section 3.2, the generated cores are explicitly added to the accumulated set of cores and thus as individual constraints to the hitting set IP. In compact symmetric core learning, detailed in Section 3.3, the generated cores are instead more compactly encoded with a small number of linear constraints that are then added to the hitting set IP instead of the cores themselves.

In explicit symmetric core learning, the cores generated via symmetries are directly (or explicitly) added to the hitting set IP as individual constraints. Algorithm 2 details our breadth-first style implementation of explicit symmetric core learning. Given a core $C$ computed by Extract-Core in the current iteration of IHS search, the set $𝒦$ of all cores found during search and a set $\mathrm{\Sigma }$ of core-preserving symmetries, Explicit-SCL first initialises a set $S$ of cores that are symmetric to $C$, and a queue $coreQueue$ of cores to be processed on Line 2. Then, the algorithm enters the while-loop between Lines 3 and 8, during which the cores in $coreQueue$ are processed in breadth-first order as follows. For a core $C$, the algorithm iterates through each symmetry $\sigma \in \mathrm{\Sigma }$. If $\sigma (C)$ is a previously unseen core, $\sigma (C)$ is added to the set $S$ and pushed into $coreQueue$ to be processed later. After adding a new core to $S$ the algorithm checks for two termination criteria: whether $|S|$, the number of new symmetric cores that have been generated, exceeds a user-defined parameter $constrLim$, and whether ${\sum }_{C\in S}|\text{lit}(C)|$, the sum of the number of literals in the new symmetric cores, exceeds the parameter $litLim$. As detailed in the following, these early termination criteria are employed to escape situations in which Algorithm 2 would otherwise produce an excessive number of symmetric cores to the point that overall search performance could suffer.

A central challenge in realizing explicit symmetric core learning is that naively applying symmetries to cores may result in a very large set of cores that do not help the IHS search terminate faster. More precisely, while a single core with $n$ literals can, in theory, generate a number of symmetric cores exponential in $n$ (e.g., in a degenerate case where any permutation of variables is a symmetry), the following observations demonstrate that the effect of explicit symmetric core learning on IHS search depends on the PBO instance. The first observation demonstrates how explicit symmetric core learning can reduce the number of iterations of the IHS main loop.

The next observation demonstrates that IHS with unrestricted explicit symmetric core learning can lead to the extraction of unnecessarily many cores during IHS search.

In contrast to the simple instance in Observation 6, in practical settings adding too many constraints to the hitting set IP can significantly increase the time needed to compute a minimum-cost solution. Identifying which cores allow IHS to make fast progress towards termination is an open research challenge. We limit explicit SCL in attempt to balance between harnessing the potential of symmetric cores to speed up search (Observation 5) and mitigating the risk of having to spent unnecessary effort to extract cores (Observation 6).

Compact symmetric core learning aims to express a large number of symmetric cores with a smaller number of constraints in the hitting set IP, making use of linear constraints native to IP. The following examples provide intuition for the approach.

As the minimum-cost solutions to the extracted cores are computed with an IP solver, we are not restricted to using binary variables for expressing a set of cores. Indeed, integer variables can be employed for representing sets of symmetric cores more compactly.

We continue with a high-level description of compact SCL. Assume that we partition a core $C={\sum }_{\mathrm{\ell }}{a}^{\mathrm{\ell }}\mathrm{\ell }\ge B$ as ${\sum }_{\mathrm{\ell }\in S}{a}^{\mathrm{\ell }}\mathrm{\ell }+{\sum }_{\mathrm{\ell }\notin S}{a}^{\mathrm{\ell }}\mathrm{\ell }\ge B$ for a subset $S$ of its literals. Now assume a set $\mathrm{\Sigma }$ of symmetries for which $\sigma ({\sum }_{\mathrm{\ell }\notin S}{a}^{\mathrm{\ell }}\mathrm{\ell })={\sum }_{\mathrm{\ell }\notin S}{a}^{\mathrm{\ell }}\mathrm{\ell }$ for each $\sigma \in \mathrm{\Sigma }$. Consider the orbit $𝒪({\sum }_{\mathrm{\ell }\in S}{a}^{\mathrm{\ell }}\mathrm{\ell },\mathrm{\Sigma })$ of the partition of the constraint containing the literals in $S$. Compact symmetric core learning generates a compact representation for a set of cores implied by $C$ and $\mathrm{\Sigma }$ by replacing ${\sum }_{\mathrm{\ell }\in S}{a}^{\mathrm{\ell }}\mathrm{\ell }$ with an integer variable $s_S$ and the definition $s_S\le \min (𝒪({\sum }_{\mathrm{\ell }\in S}{a}^{\mathrm{\ell }}\mathrm{\ell },\mathrm{\Sigma }))$. In the rest of this section, we fill in the details of this high-level description of compact SCL.

As illustrated in Examples 7 and 8, compact SCL can substitute several subsets of a core with new variables and in doing so represent many symmetric cores more compactly. What is happening in these examples is that (certain) subgroups of the group of all symmetries act independently on parts of the core rather than on the whole core. However, as the following observation shows, independent rewriting of parts of the cores is not sound in case symmetries interact too much. In the rest of this section, we will formalize conditions that guarantee the soundness of rewriting parts of the core.

Observation 9 demonstrates that the choice of symmetries under which to compute orbits can not be done independently for all subsets to be replaced. One way to interpret Observation 9 is that if we wish to introduce a new variable defined by the orbit ${𝒪}_2$ into a core that already has another new variable defined by the orbit ${𝒪}_1$, we need to ensure that the symmetries used to compute the orbit ${𝒪}_2$ “behave well” together with those used to compute ${𝒪}_1$. The following definition formalizes this notion of well-behavedness.

For intuition on Definition 10, assume that we are computing a compact representation for a set of cores symmetric to $C$ partitioned as $L_1+\mathrm{\cdots }+L_k\ge A$. If we process the partitions in the order of $L_1,L_2,\mathrm{\dots },L_k$, then a symmetry decomposition of $C$ defines which symmetries we apply to generate the orbit ${𝒪}_i$ for each $L_i$. To be a symmetry decomposition, we should be able to split our core so that each symmetry in the $i^{\text{th}}$ set stabilizes the parts of the core beyond $i$ as well as the orbits in all of the earlier parts of the core. These conditions together guarantee that every constraint represented by the compact representation is a core.

Practical implementations of IHS employ various additional heuristic optimizations which are central for runtime efficiency. This is also the case for PBO-IHS. The two heuristics that affect our implementation of SCL are forms of hardening, including reduced cost fixing [5] and weight-aware core extraction (WCE) [14, 8].

Hardening refers to fixing the value of an objective literal $\mathrm{\ell }$ during search. There are two ways in which that can happen: (i) if the coefficient of $\mathrm{\ell }$ is strictly greater than the current upper-bound $ub$, then the literal is fixed to $0$ since setting it to $1$ would lead to a worse solution than the current best known; or (ii) via reduced cost fixing [5], i.e., if the reduced cost of $\mathrm{\ell }$ in the LP relaxation of the hitting set IP detailed in Figure 1 imply that $\mathrm{\ell }$ is set either to $0$ or $1$ in the optimal solutions. Hardening affects SCL in that symmetries that map non-fixed literals to fixed ones are removed from $\mathrm{\Sigma }$ when symmetric cores are generated.

Weight-aware core extraction aims to delay calls to Min-Sol by extracting multiple cores falsified by a solution $\gamma$ in each iteration. Intuitively this decreases the number of times that the hitting set IP needs to be solved [38, 37]. With SCL, we interleave the calls to the SCL procedure between the core-extraction steps: after Extract-Core obtains each new core $C$, we compute symmetric cores to it and then invoke Extract-Core again, asking for a core that is falsified by $\gamma$ and not any of the cores that have been computed in this iteration. In practice, this is achieved by removing at least one literal from every obtained core from the assumptions posed in the next query to Extract-Core. The Min-Sol procedure is invoked only when Extract-Core does not find more cores.

We end this section with a short observation comparing SCL and symmetry breaking with lex-leader constraints in the context of IHS. In contrast to SCL, symmetry breaking with lex-leader constraints does not result in the IHS search extracting more of the original cores of the PBO instance, but rather introduces new cores that change the search.

We start by considering two examples of problem domains known to have a high number of symmetries intrinsically. The first, which we will refer to as the CC problem, asks to maximize the size of the largest clique over all graphs with $n$ nodes that admit a $k$-coloring where $n$ and $k$ are given parameters. Additionally, we consider a variant of the problem in which all nodes are given a distinct weight from $1,\mathrm{\dots },n$, and the task is to maximize sum-of-weights of the nodes in the clique. We will refer to this variant as “weighted CC” and talk about “unweighted CC” when the task is to maximize the size of the clique. In our experiments, we use an extension of the encoding from [29] to optimization, the full details of the encoding are in Appendix B. Beyond being highly symmetric (as explained in short), the CC problem draws motivations from proof complexity: tautologies of the type “a graph either does not contain a clique of size $m$, or is not $(m-1)$-colorable”, expressed similarly to the encoding we use, are exponentially hard for cutting planes [29].

Note that the size of the largest clique in the graphs that admit a $k$-coloring is $k$. There are many symmetric variants of graphs with $n$ nodes that admit both a $k$-coloring and a clique of size $k$. The encoding of CC results in PBO instances in which the objective contains $n$ variables that are indicators for a node not being included in the clique. With this intuition, any at-least-one core corresponds to a subset of nodes that cannot all be included in the clique. Since the maximum size of the clique is $k$, it follows that any subset of nodes that contains $k+1$ nodes corresponds to a (subset-minimal) core. Termination of IHS using only cores of this form requires in total $\left(\genfrac{}{}{0pt}{}{n}{k+1}\right)$ cores that rule out all such subsets from consideration.

The CC instances contain two types of easy-to-grasp symmetries: “node-symmetries” over the node indices, and “color-symmetries” over color indices. Both types are present in weighted and unweighted CC, but very notably, the node-symmetries that, informally speaking, map nodes to other nodes are strong only in the unweighted variant. To see this, observe that mapping nodes to other nodes preserves the cost of solutions only in the unweighted case. When invoked on the PB encoding of the CC problem (unweighted or weighted) explicit SCL, using the node-symmetries and a single minimal at-least-one core of size $k+1$, can generate $\left(\genfrac{}{}{0pt}{}{n}{k+1}\right)-1$ other cores corresponding to all other $\left(\genfrac{}{}{0pt}{}{n}{k+1}\right)-1$ subsets of size $k+1$. As such, IHS with explicit SCL can terminate after extracting a single core from Extract-Core, but enumerates an exponential number of symmetric cores and adds them to the hitting set IP. In contrast, given one core of size $k+1$, and the node-symmetries, compact SCL can generate a single cardinality constraint that limits the maximum number of nodes in any clique to $k$, resulting in termination of IHS in the next iteration with only a single constraint added to the hitting set IP.

Regarding lex-leader-based symmetry breaking on unweighted CC instances, if the node-symmetries are broken completely (which is not guaranteed to be the case, but is a best-case scenario that LL heuristically aims to achieve), the additional constraints added to the PBO instance essentially enforce that the maximum clique consists of $k$ specific nodes instead of any $k$ nodes. Then the instance extended with lex-leader constraints has $n-k$ unit cores that directly enforce that the other nodes can not be in the maximum clique. When invoked on the extended instance, IHS can terminate after extracting $n-k$ of these (short) cores. (On weighted CC instances, the node-symmetries can be broken quite similarly when weak symmetry detection and dominance constraints are used: then the constraints enforce that the maximum clique consists of the $k$ nodes with largest weights.) Further, in contrast to SCL, the fact that lex-leader symmetry breaking adds constraints to core-extractor can decrease core-extraction times. Thus we expect symmetry breaking to be very effective in these instances. The main question is how close IHS with (explicit/compact) SCL comes to the performance of IHS with lex-leader symmetry breaking.

To experiment with CC, we generated instances with all combinations of $n=\mathrm{5..29}$ and $k=2..n$, yielding a total of $400$ unweighted and $400$ weighted benchmarks. On unweighted CC (see Figure 2 left), explicit SCL solves 16 more instances than the Baseline (IHS without symmetry techniques) with 69 vs 53 solved benchmarks. Compact SCL is even more effective, solving $6$ more instances than explicit SCL (75 vs 69 instances). Using lex-leader with the full set of weak symmetries (LL) leads to 68 instances solved, which is less than either variant of SCL. Interestingly, restricting lex-leader-based symmetry breaking to the set of strong symmetries (LLS in the figure) leads to the overall best performance on unweighted CC and 104 instances solved. The results suggest that restricting the types of symmetries that BreakID can find (in this case to symmetries that map objective variables to objective variables), allows for better recognition of the relevant structure of the instance.

On the weighted CC instances (Figure 2 middle) the baseline solves 60 instances and lex-leader symmetry breaking restricted to strong symmetries only marginally improves with 62. When allowed to use all weak symmetries, IHS with lex-leader symmetry breaking improves to 71 solved instances. Our SCL approaches obtain the best performance and notable improvements over lex-leader-based breaking; explicit SCL solves 73 instances and compact SCL an impressive 77. A potential explanation for the big difference in performance of LLS between the unweighted and the weighted case is that node-symmetries are not strong in the weighted variant (whereas they are in the unweighted).

As a second, more practically oriented highly symmetric problem domain, we consider haplotype inference pedigrees problem [22], and in particular the task of finding a set of haplotypes that best explains given set of genotypes. For experimenting with this problem domain, we used the $100$ instances submitted to Pseudo-Boolean competition 2011. It should be noted that, as explained in [22], these instances already include domain-specific symmetry breaking constraints added by hand for increased performance, enforcing a predefined order for the two haplotypes that produce a genotype. Hence an interesting question is whether the different symmetry techniques can improve IHS performance further on these instances. Again, (compact) SCL provides the greatest performance improvements (see Figure 2 right): Baseline without symmetry breaking solves 66 instances, which is improved by lex-leader symmetry breaking to 68 instances by both variants, LL and LLS – however, with explicit SCL the number of solved instances goes up to 74, and with compact SCL further to 76.

We also investigate the relative impact of lex-leader symmetry breaking and SCL more generally on a wide set of PBO benchmarks including instances from over 60 domains as used in the the original papers presenting PBO-IHS [37, 38]. Our main interest here is whether the different types of symmetry techniques are viable to use by default even when there are no guarantees that the input instances would be highly symmetric. The benchmark set consists of $1786$ instances across tens of different benchmark domains; see [36] for more details. We disregard LL here since LLS turned out to perform better than LL (see Appendix C).

A pairwise per-instance runtime comparison of Baseline, LLS and ExplicitSCL is shown in Figure 3. The total number of instances solved is: Baseline 948, LLS 947, ExplicitSCL 954, and CompactSCL 947. LLS results in significant runtime degradation compared to Baseline (Figure 3 top left). Indeed, the impact lex-leader symmetry breaking has on PBO-IHS appears very different to results presented in [40] on the runtime impact of lex-leader symmetry breaking on other PBO solving approaches, where (mild) runtime improvements were reported. ExplicitSCL consistently and most often significantly outperforms LLS (Figure 3 bottom left). A reason for this is that the PB solver used for core extraction tends to use significantly more time when invoked on a satisfiable instance. This follows the intuition that, in contrast to the dynamically applied SCL, the lex-leader constraints all added in the beginning of IHS search rule out symmetric solutions and hence may make finding solutions more difficult; more details on the runtime differences are provided in Appendix D. Similarly, ExplicitSCL on most instances significantly outperforms LLS (Figure 3 bottom left). ExplicitSCL also tends to have a performance-improvement impact on PBO-IHS, as observed in Figure 3 (top right), despite the symmetry computation overhead (up to $100$ s). In contrast, despite CompactSCL performing very well on selected highly symmetric domains (recall Section 4.1), on this wider heterogenous set of benchmarks, CompactSCL performs slightly worse compared to ExplicitSCL (Figure 3 bottom right).

ExplicitSCL tends to terminate with fewer IHS main loop iterations than Baseline (Figure 4 left), suggesting that symmetric cores added by SCL are indeed helpful in decreasing required number of core extraction steps. Between ExplicitSCL and CompactSCL, there appear to be only more minor differences both ways (Figure 4 middle left). The relative number of iterations between LLS and ExplicitSCL (Figure 4 middle right) and LLS and Baseline (Figure 4 top left) do not fully explain the runtime degradation caused by LLS (recall Figure 3 right), which suggests that lex-leader constraints indeed significantly slow down the IHS iterations on average.