Christopher Jefferson

Özgür Akgün, Mun See Chang, Ian P. Gent et al.

In constraint programming and related paradigms, a modeller specifies their problem in a modelling language for a solver to search and return its solution(s). Using high-level modelling languages such as Essence, a modeller may express their problems in terms of abstract structures. These are structures not natively supported by the solvers, and so they have to be transformed into or represented as other structures before solving. For example, nested sets are abstract structures, and they can be represented as matrices in constraint solvers. Many problems contain symmetries and one very common and highly successful technique used in constraint programming is to "break" symmetries, to avoid searching for symmetric solutions. This can speed up the solving process by many orders of magnitude. Most of these symmetry-breaking techniques involve placing some kind of ordering for the variables of the problem, and picking a particular member under the symmetries, usually the smallest. Unfortunately, applying this technique to abstract variables produces a very large number of complex constraints that perform poorly in practice. In this paper, we demonstrate a new incomplete method of breaking the symmetries of abstract structures by better exploiting their representations. We apply the method in breaking the symmetries arising from indistinguishable objects, a commonly occurring type of symmetry, and show that our method is faster than the previous methods proposed in (Akgün et al. 2025).

Ozgur Akgun, Mun See Chang, Ian P. Gent et al.

Indistinguishable objects often occur when modelling problems in constraint programming, as well as in other related paradigms. They occur when objects can be viewed as being drawn from a set of unlabelled objects, and the only operation allowed on them is equality testing. For example, the golfers in the social golfer problem are indistinguishable. If we do label the golfers, then any relabelling of the golfers in one solution gives another valid solution. Therefore, we can regard the symmetric group of size $n$ as acting on a set of $n$ indistinguishable objects. In this paper, we show how we can break the symmetries resulting from indistinguishable objects. We show how symmetries on indistinguishable objects can be defined properly in complex types, for example in a matrix indexed by indistinguishable objects. We then show how the resulting symmetries can be broken correctly. In Essence, a high-level modelling language, indistinguishable objects are encapsulated in "unnamed types". We provide an implementation of complete symmetry breaking for unnamed types in Essence.

Özgür Akgün, Ian P. Gent, Christopher Jefferson et al.

The performance of a constraint model can often be improved by converting a subproblem into a single table constraint (referred to as tabulation). Finding subproblems to tabulate is traditionally a manual and time-intensive process, even for expert modellers. This paper presents TabID, an entirely automated method to identify promising subproblems for tabulation in constraint programming. We introduce a diverse set of heuristics designed to identify promising candidates for tabulation, aiming to improve solver performance. These heuristics are intended to encapsulate various factors that contribute to useful tabulation. We also present additional checks to limit the potential drawbacks of suboptimal tabulation. We comprehensively evaluate our approach using benchmark problems from existing literature that previously relied on manual identification by constraint programming experts of constraints to tabulate. We demonstrate that our automated identification and tabulation process achieves comparable, and in some cases improved results. We empirically evaluate the efficacy of our approach on a variety of solvers, including standard CP (Minion and Gecode), clause-learning CP (Chuffed and OR-Tools) and SAT solvers (Kissat). Our findings highlight the substantial potential of fully automated tabulation, suggesting its integration into automated model reformulation tools.

Özgür Akgün, Alan M. Frisch, Ian P. Gent et al.

The Essence language allows a user to specify a constraint problem at a level of abstraction above that at which constraint modelling decisions are made. Essence specifications are refined into constraint models using the Conjure automated modelling tool, which employs a suite of refinement rules. However, Essence is a rich language in which there are many equivalent ways to specify a given problem. A user may therefore omit the use of domain attributes or abstract types, resulting in fewer refinement rules being applicable and therefore a reduced set of output models from which to select. This paper addresses the problem of recovering this information automatically to increase the robustness of the quality of the output constraint models in the face of variation in the input Essence specification. We present reformulation rules that can change the type of a decision variable or add attributes that shrink its domain. We demonstrate the efficacy of this approach in terms of the quantity and quality of models Conjure can produce from the transformed specification compared with the original.

Joan Espasa, Ian P. Gent, Ruth Hoffmann et al.

In this paper, we present Demystify, a general tool for creating human-interpretable step-by-step explanations of how to solve a wide range of pen and paper puzzles from a high-level logical description. Demystify is based on Minimal Unsatisfiable Subsets (MUSes), which allow Demystify to solve puzzles as a series of logical deductions by identifying which parts of the puzzle are required to progress. This paper makes three contributions over previous work. First, we provide a generic input language, based on the Essence constraint language, which allows us to easily use MUSes to solve a much wider range of pen and paper puzzles. Second, we demonstrate that the explanations that Demystify produces match those provided by humans by comparing our results with those provided independently by puzzle experts on a range of puzzles. We compare Demystify to published guides for solving a range of different pen and paper puzzles and show that by using MUSes, Demystify produces solving strategies which closely match human-produced guides to solving those same puzzles (on average 89% of the time). Finally, we introduce a new randomised algorithm to find MUSes for more difficult puzzles. This algorithm is focused on optimised search for individual small MUSes.

Peter Nightingale, Ian Philip Gent, Christopher Jefferson et al.

Special-purpose constraint propagation algorithms frequently make implicit use of short supports -- by examining a subset of the variables, they can infer support (a justification that a variable-value pair may still form part of an assignment that satisfies the constraint) for all other variables and values and save substantial work -- but short supports have not been studied in their own right. The two main contributions of this paper are the identification of short supports as important for constraint propagation, and the introduction of HaggisGAC, an efficient and effective general purpose propagation algorithm for exploiting short supports. Given the complexity of HaggisGAC, we present it as an optimised version of a simpler algorithm ShortGAC. Although experiments demonstrate the efficiency of ShortGAC compared with other general-purpose propagation algorithms where a compact set of short supports is available, we show theoretically and experimentally that HaggisGAC is even better. We also find that HaggisGAC performs better than GAC-Schema on full-length supports. We also introduce a variant algorithm HaggisGAC-Stable, which is adapted to avoid work on backtracking and in some cases can be faster and have significant reductions in memory use. All the proposed algorithms are excellent for propagating disjunctions of constraints. In all experiments with disjunctions we found our algorithms to be faster than Constructive Or and GAC-Schema by at least an order of magnitude, and up to three orders of magnitude.