Christopher Jefferson

AAAI Conference 2026 Conference Paper

Faster Symmetry Breaking Constraints for Abstract Structures

• Özgür Akgün
• Mun See Chang
• Ian P. Gent
• Christopher Jefferson

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).

AIJ Journal 2025 Journal Article

Athanor: Local search over abstract constraint specifications

• Saad Attieh
• Nguyen Dang
• Christopher Jefferson
• Ian Miguel
• Peter Nightingale

Local search is a common method for solving combinatorial optimisation problems. We focus on general-purpose local search solvers that accept as input a constraint model — a declarative description of a problem consisting of a set of decision variables under a set of constraints. Existing approaches typically take as input models written in solver-independent constraint modelling languages like MiniZinc. The Athanor solver we describe herein differs in that it begins from a specification of a problem in the abstract constraint specification language Essence , which allows problems to be described without commitment to low-level modelling decisions through its support for a rich set of abstract types. The advantage of proceeding from Essence is that the structure apparent in a concise, abstract specification of a problem can be exploited to generate high quality neighbourhoods automatically, avoiding the difficult task of identifying that structure in an equivalent constraint model. Based on the twin benefits of neighbourhoods derived from high level types and the scalability derived by searching directly over those types, our empirical results demonstrate strong performance in practice relative to existing solution methods.

JAIR Journal 2025 Journal Article

TabID: Automatic Identification and Tabulation of Subproblems in Constraint Models

• Özgür Akgün
• Ian Gent
• Christopher Jefferson
• Zeynep Kiziltan
• Ian Miguel
• Peter Nightingale
• András Z. Salamon
• Felix Ulrich-Oltean

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.

IJCAI Conference 2023 Conference Paper

Conjure: Automatic Generation of Constraint Models from Problem Specifications (Extended Abstract)

• Özgür Akgün
• Alan M. Frisch
• Ian P. Gent
• Christopher Jefferson
• Ian Miguel
• Peter Nightingale

When solving a combinatorial problem, the formulation or model of the problem is critical to the efficiency of the solver. Automating the modelling process has long been of interest given the expertise and time required to develop an effective model of a particular problem. We describe a method to automatically produce constraint models from a problem specification written in the abstract constraint specification language Essence. Our approach is to incrementally refine the specification into a concrete model by applying a chosen refinement rule at each step. Any non-trivial specification may be refined in multiple ways, creating a diverse space of models to choose from. The handling of symmetries is a particularly important aspect of automated modelling. We show how modelling symmetries may be broken automatically as they enter a model during refinement, removing the need for an expensive symmetry detection step following model formulation. Our approach is implemented in a system called Conjure. We compare the models produced by Conjure to constraint models from the literature that are known to be effective. Our empirical results confirm that Conjure can reproduce successfully the kernels of the constraint models of 42 benchmark problems found in the literature.

AIJ Journal 2022 Journal Article

Conjure: Automatic Generation of Constraint Models from Problem Specifications

• Özgür Akgün
• Alan M. Frisch
• Ian P. Gent
• Christopher Jefferson
• Ian Miguel
• Peter Nightingale

When solving a combinatorial problem, the formulation or model of the problem is critical to the efficiency of the solver. Automating the modelling process has long been of interest because of the expertise and time required to produce an effective model of a given problem. We describe a method to automatically produce constraint models from a problem specification written in the abstract constraint specification language Essence. Our approach is to incrementally refine the specification into a concrete model by applying a chosen refinement rule at each step. Any non-trivial specification may be refined in multiple ways, creating a space of models to choose from. The handling of symmetries is a particularly important aspect of automated modelling. Many combinatorial optimisation problems contain symmetry, which can lead to redundant search. If a partial assignment is shown to be invalid, we are wasting time if we ever consider a symmetric equivalent of it. A particularly important class of symmetries are those introduced by the constraint modelling process: modelling symmetries. We show how modelling symmetries may be broken automatically as they enter a model during refinement, obviating the need for an expensive symmetry detection step following model formulation. Our approach is implemented in a system called Conjure. We compare the models produced by Conjure to constraint models from the literature that are known to be effective. Our empirical results confirm that Conjure can reproduce successfully the kernels of the constraint models of 42 benchmark problems found in the literature.

IJCAI Conference 2019 Conference Paper

Athanor: High-Level Local Search Over Abstract Constraint Specifications in Essence

• Saad Attieh
• Nguyen Dang
• Christopher Jefferson
• Ian Miguel
• Peter Nightingale

This paper presents Athanor, a novel local search solver that operates on abstract constraint specifications of combinatorial problems in the Essence language. It is unique in that it operates directly on the high level, nested types in Essence, such as set of partitions or multiset of sequences, without refining such types into low level representations. This approach has two main advantages. First, the structure present in the high level types allows high quality neighbourhoods for local search to be automatically derived. Second, it allows Athanor to scale much better than solvers that operate on the equivalent, but much larger, low-level representations. The paper details how Athanor operates, covering incremental evaluation, dynamic unrolling of quantified expressions and neighbourhood construction. A series of case studies show the performance of Athanor, benchmarked against several local search solvers on a range of problem classes.

IJCAI Conference 2018 Conference Paper

A Framework for Constraint Based Local Search using Essence

• Özgür Akgün
• Saad Attieh
• Ian P. Gent
• Christopher Jefferson
• Ian Miguel
• Peter Nightingale
• András Z. Salamon
• Patrick Spracklen

Structured Neighbourhood Search (SNS) is a framework for constraint-based local search for problems expressed in the Essence abstract constraint specification language. The local search explores a structured neighbourhood, where each state in the neighbourhood preserves a high level structural feature of the problem. SNS derives highly structured problem-specific neighbourhoods automatically and directly from the features of the Essence specification of the problem. Hence, neighbourhoods can represent important structural features of the problem, such as partitions of sets, even if that structure is obscured in the low-level input format required by a constraint solver. SNS expresses each neighbourhood as a constrained optimisation problem, which is solved with a constraint solver. We have implemented SNS, together with automatic generation of neighbourhoods for high level structures, and report high quality results for several optimisation problems.

IJCAI Conference 2018 Conference Paper

Complexity of n-Queens Completion (Extended Abstract)

• Ian P. Gent
• Christopher Jefferson
• Peter Nightingale

The n-Queens problem is to place n chess queens on an n by n chessboard so that no two queens are on the same row, column or diagonal. The n-Queens Completion problem is a variant, dating to 1850, in which some queens are already placed and the solver is asked to place the rest, if possible. We show that n-Queens Completion is both NP-Complete and #P-Complete. A corollary is that any non-attacking arrangement of queens can be included as a part of a solution to a larger n-Queens problem. We introduce generators of random instances for n-Queens Completion and the closely related Blocked n-Queens and Excluded Diagonals Problem. We describe three solvers for these problems, and empirically analyse the hardness of randomly generated instances. For Blocked n-Queens and the Excluded Diagonals Problem, we show the existence of a phase transition associated with hard instances as has been seen in other NP-Complete problems, but a natural generator for n-Queens Completion did not generate consistently hard instances. The significance of this work is that the n-Queens problem has been very widely used as a benchmark in Artificial Intelligence, but conclusions on it are often disputable because of the simple complexity of the decision problem. Our results give alternative benchmarks which are hard theoretically and empirically, but for which solving techniques designed for n-Queens need minimal or no change.

AIJ Journal 2017 Journal Article

Automatically improving constraint models in Savile Row

• Peter Nightingale
• Özgür Akgün
• Ian P. Gent
• Christopher Jefferson
• Ian Miguel
• Patrick Spracklen

When solving a combinatorial problem using Constraint Programming (CP) or Satisfiability (SAT), modelling and formulation are vital and difficult tasks. Even an expert human may explore many alternatives in modelling a single problem. We make a number of contributions in the automated modelling and reformulation of constraint models. We study a range of automated reformulation techniques, finding combinations of techniques which perform particularly well together. We introduce and describe in detail a new algorithm, X-CSE, to perform Associative–Commutative Common Subexpression Elimination (AC-CSE) in constraint problems, significantly improving existing CSE techniques for associative and commutative operators such as +. We demonstrate that these reformulation techniques can be integrated in a single automated constraint modelling tool, called Savile Row, whose architecture we describe. We use Savile Row as an experimental testbed to evaluate each reformulation on a set of 50 problem classes, with 596 instances in total. Our recommended reformulations are well worthwhile even including overheads, especially on harder instances where solver time dominates. With a SAT solver we observed a geometric mean of 2. 15 times speedup compared to a straightforward tailored model without recommended reformulations. Using a CP solver, we obtained a geometric mean of 5. 96 times speedup for instances taking over 10 seconds to solve.

JAIR Journal 2017 Journal Article

Complexity of n-Queens Completion

• Ian P. Gent
• Christopher Jefferson
• Peter Nightingale

The n-Queens problem is to place n chess queens on an n by n chessboard so that no two queens are on the same row, column or diagonal. The n-Queens Completion problem is a variant, dating to 1850, in which some queens are already placed and the solver is asked to place the rest, if possible. We show that n-Queens Completion is both NP-Complete and #P-Complete. A corollary is that any non-attacking arrangement of queens can be included as a part of a solution to a larger n-Queens problem. We introduce generators of random instances for n-Queens Completion and the closely related Blocked n-Queens and Excluded Diagonals Problem. We describe three solvers for these problems, and empirically analyse the hardness of randomly generated instances. For Blocked n-Queens and the Excluded Diagonals Problem, we show the existence of a phase transition associated with hard instances as has been seen in other NP-Complete problems, but a natural generator for n-Queens Completion did not generate consistently hard instances. The significance of this work is that the n-Queens problem has been very widely used as a benchmark in Artificial Intelligence, but conclusions on it are often disputable because of the simple complexity of the decision problem. Our results give alternative benchmarks which are hard theoretically and empirically, but for which solving techniques designed for n-Queens need minimal or no change.

SoCS Conference 2016 Conference Paper

A Theoretical Framework for Constraint Propagator Triggering

• David A. Cohen
• Christopher Jefferson
• Karen E. Petrie

CSP instances are commonly solved by backtracking search combined with constraint propagation. During search, constraint solvers aim to remove any literals (variable-value pair) that can be shown not to be part of any solution. This literal removal, called propagation, is the beating heart of modern constraint solvers. A significant proportion of the runtime of propagating constraint solvers is spent running propagation algorithms. Therefore any mechanism for reducing how frequently propagators are called leads directly to significant performance improvements. One family of popular techniques is dynamic triggering — these techniques aim to avoid invoking a propagator when it would remove no literals. While this technique has been successful in practice, it has not yet been studied theoretically. This paper provides a theoretical framework for understanding when dynamic triggering will be successful. In particular, we prove when a literal deletion does not require a propagator to be executed. To achieve this, we describe supports: a support for a constraint is a set of literals whose presence in a search state ensures that propagating the constraint will not remove any literals. Therefore running the propagator when a literal outside the support is deleted is a waste of time. By characterising supports and giving a definition of dynamic and static supports for the CSP, we provide the framework for a proper analysis. We show how the number of triggers required for different constraints varies widely. For some constraints, dynamic triggering allows very small supports, for others the number of required supports is provably large.

ECAI Conference 2014 Conference Paper

Breaking Conditional Symmetry in Automated Constraint Modelling with CONJURE

• Özgür Akgün
• Ian P. Gent
• Christopher Jefferson
• Ian Miguel
• Peter Nightingale

Many constraint problems contain symmetry, which can lead to redundant search. If a partial assignment is shown to be invalid, we are wasting time if we ever consider a symmetric equivalent of it. A particularly important class of symmetries are those introduced by the constraint modelling process: model symmetries. We present a systematic method by which the automated constraint modelling tool CONJURE can break conditional symmetry as it enters a model during refinement. Our method extends, and is compatible with, our previous work on automated symmetry breaking in CONJURE. The result is the automatic and complete removal of model symmetries for the entire problem class represented by the input specification. This applies to arbitrarily nested conditional symmetries and represents a significant step forward for automated constraint modelling.

AIJ Journal 2014 Journal Article

Generating custom propagators for arbitrary constraints

• Ian P. Gent
• Christopher Jefferson
• Steve Linton
• Ian Miguel
• Peter Nightingale

Constraint Programming (CP) is a proven set of techniques for solving complex combinatorial problems from a range of disciplines. The problem is specified as a set of decision variables (with finite domains) and constraints linking the variables. Local reasoning (propagation) on the constraints is central to CP. Many constraints have efficient constraint-specific propagation algorithms. In this work, we generate custom propagators for constraints. These custom propagators can be very efficient, even approaching (and in some cases exceeding) the efficiency of hand-optimised propagators. Given an arbitrary constraint, we show how to generate a custom propagator that establishes GAC in small polynomial time. This is done by precomputing the propagation that would be performed on every relevant subdomain. The number of relevant subdomains, and therefore the size of the generated propagator, is potentially exponential in the number and domain size of the constrained variables. The limiting factor of our approach is the size of the generated propagators. We investigate symmetry as a means of reducing that size. We exploit the symmetries of the constraint to merge symmetric parts of the generated propagator. This extends the reach of our approach to somewhat larger constraints, with a small run-time penalty. Our experimental results show that, compared with optimised implementations of the table constraint, our techniques can lead to an order of magnitude speedup. Propagation is so fast that the generated propagators compare well with hand-written carefully optimised propagators for the same constraints, and the time taken to generate a propagator is more than repaid.

IJCAI Conference 2013 Conference Paper

Extending Simple Tabular Reduction with Short Supports

• Christopher Jefferson
• Peter Nightingale

Monte-Carlo Tree Search (MCTS) has proved a remarkably effective decision mechanism in many different game domains, including computer Go and general game playing (GGP). However, in GGP, where many disparate games are played, certain type of games have proved to be particularly problematic for MCTS. One of the problems are game trees with so-called optimistic moves, that is, bad moves that superficially look good but potentially require much simulation effort to prove otherwise. Such scenarios can be difficult to identify in real time and can lead to suboptimal or even harmful decisions. In this paper we investigate a selection strategy for MCTS to alleviate this problem. The strategy, called sufficiency threshold, concentrates simulation effort better for resolving potential optimistic move scenarios. The improved strategy is evaluated empirically in an n-arm-bandit test domain for highlighting its properties as well as in a state-of-the-art GGP agent to demonstrate its effectiveness in practice. The new strategy shows significant improvements in both domains.

IJCAI Conference 2013 Conference Paper

Extending Simple Tabular Reduction with Short Supports

• Christopher Jefferson
• Peter Nightingale

Constraint propagation is one of the key techniques in constraint programming, and a large body of work has built up around it. 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 still forms part of a solution to the constraint) for all other variables and values and save substantial work. Recently short supports have been used in general purpose propagators, and (when the constraint is amenable to short supports) speed ups of more than three orders of magnitude have been demonstrated. In this paper we present SHORTSTR2, a development of the Simple Tabular Reduction algorithm STR2+. We show that SHORTSTR2 is complementary to the existing algorithms SHORTGAC and HAGGISGAC that exploit short supports, while being much simpler. When a constraint is amenable to short supports, the short support set can be exponentially smaller than the full-length support set. Therefore SHORTSTR2 can efficiently propagate many constraints that STR2+ cannot even load into memory. We also show that SHORTSTR2 can be combined with a simple algorithm to identify short supports from full-length supports, to provide a superior drop-in replacement for STR2+.

IJCAI Conference 2011 Conference Paper

Exploiting Short Supports for Generalised Arc Consistency for Arbitrary Constraints

• Peter Nightingale
• Ian P. Gent
• Christopher Jefferson
• Ian Miguel

Special-purpose constraint propagation algorithms (such as those for the element constraint) frequently make implicit use of short supports - by examining a subset of the variables, they can infer support for all other variables and values and save substantial work. However, to date general purpose propagation algorithms (such as GAC-Schema) rely upon supports involving all variables. We demonstrate how to employ short supports in a new general purpose propagation algorithm called ShortGAC. This works when provided with either an explicit list of allowed short tuples, or a function to calculate the next supporting short tuple. Empirical analyses demonstrate the efficiency of ShortGAC compared to other general-purpose propagation algorithms. In some cases ShortGAC even exhibits similar performance to special-purpose propagators.

AIJ Journal 2010 Journal Article

Implementing logical connectives in constraint programming

• Christopher Jefferson
• Neil C.A. Moore
• Peter Nightingale
• Karen E. Petrie

Combining constraints using logical connectives such as disjunction is ubiquitous in constraint programming, because it adds considerable expressive power to a constraint language. We explore the solver architecture needed to propagate such combinations of constraints efficiently. In particular we describe two new features named satisfying sets and constraint trees. We also make use of movable triggers (Gent et al. , 2006) [1], and with these three complementary features we are able to make considerable efficiency gains. A key reason for the success of Boolean Satisfiability (SAT) solvers is their ability to propagate Or constraints efficiently, making use of movable triggers. We successfully generalise this approach to an Or of an arbitrary set of constraints, maintaining the crucial property that at most two constraints are active at any time, and no computation at all is done on the others. We also give an And propagator within our framework, which may be embedded within the Or. Using this approach, we demonstrate speedups of over 10, 000 times in some cases, compared to traditional constraint programming approaches. We also prove that the Or algorithm enforces generalised arc consistency (GAC) when all its child constraints have a GAC propagator, and no variables are shared between children. By extending the Or propagator, we present a propagator for AtLeastK, which expresses that at least k of its child constraints are satisfied in any solution. Some logical expressions (e. g. exclusive-or) cannot be compactly expressed using And, Or and AtLeastK. Therefore we investigate reification of constraints. We present a fast generic algorithm for reification using satisfying sets and movable triggers.

ECAI Conference 2010 Conference Paper

Learning When to Use Lazy Learning in Constraint Solving

• Ian P. Gent
• Christopher Jefferson
• Lars Kotthoff
• Ian Miguel
• Neil C. A. Moore
• Peter Nightingale
• Karen E. Petrie

Learning in the context of constraint solving is a technique by which previously unknown constraints are uncovered during search and used to speed up subsequent search. Recently, lazy learning, similar to a successful idea from satisfiability modulo theories solvers, has been shown to be an effective means of incorporating constraint learning into a solver. Although a powerful technique to reduce search in some circumstances, lazy learning introduces a substantial overhead, which can outweigh its benefits. Hence, it is desirable to know beforehand whether or not it is expected to be useful. We approach this problem using machine learning (ML). We show that, in the context of a large benchmark set, standard ML approaches can be used to learn a simple, cheap classifier which performs well in identifying instances on which lazy learning should or should not be used. Furthermore, we demonstrate significant performance improvements of a system using our classifier and the lazy learning and standard constraint solvers over a standard solver. Through rigorous cross-validation across the different problem classes in our benchmark set, we show the general applicability of our learned classifier.

AAAI Conference 2006 Conference Paper

Constraint Symmetry and Solution Symmetry

• David Cohen
• Christopher Jefferson

Symmetry in constraint satisfaction problems (CSPs) has been considered in two fundamentally different ways: as an operation preserving the solutions of a CSP instance, or as an operation preserving the constraints. To reflect these two views, we define solution symmetry and constraint symmetry. We discuss how these concepts are related and show that some CSP instances have many more solution symmetries than constraint symmetries.

ECAI Conference 2006 Conference Paper

Minion: A Fast Scalable Constraint Solver

• Ian P. Gent
• Christopher Jefferson
• Ian Miguel

We present Minion, a new constraint solver. Empirical results on standard benchmarks show orders of magnitude performance gains over state-of-the-art constraint toolkits. These gains increase with problem size – MINION delivers scalable constraint solving. MINION is a general-purpose constraint solver, with an expressive input language based on the common constraint modelling device of matrix models. Focussing on matrix models supports a highly-optimised implementation, exploiting the properties of modern processors. This contrasts with current constraint toolkits, which, in order to provide ever more modelling and solving options, have become progressively more complex at the cost of both performance and usability. MINION is a black box from the user point of view, deliberately providing few options. This, combined with its raw speed, makes MINION a substantial step towards Puget's ‘Model and Run’ constraint solving paradigm.

ECAI Conference 2004 Conference Paper

Symmetry Breaking as a Prelude to Implied Constraints: A Constraint Modelling Pattern

• Alan M. Frisch
• Christopher Jefferson
• Ian Miguel