The Rules of Constraint Modelling

1 Introduction

To employ finite-domain constraint programming technology to solve a problem, the problem first must be characterised, or modelled, by a set of constraints on decision variables that solutions must satisfy. Modelling can be difficult and requires expertise, thus limiting widespread use of constraint technology. The vast majority of research on constraint modelling presents alternative models to a particular problem and evaluates these alternatives through analysis and/or experiment. The process by which the alternative models are generated is rarely, if ever, discussed. Each constraint programmer must learn the art of modelling by forming generalisations from these studies.

We show that a set of rules can formalise the generation of alternative models. Doing this requires a language in which to express the abstract problem structure of which models are a function. If all modelling choices are to be open to the rules, the language must have a level of abstraction above that at which modelling decisions are made. We have designed such a language and call it ESSENCE.

The rules are embedded in the CONJURE system, which, given an ESSENCE specification, generates models of the type supported by existing constraint solvers. Hence, we refer to our rules as refinement rules. Our current focus is on generating a set of correct models that includes those that a human expert would generate. Future work will focus on generating only good models.

2 Challenges and Contributions

A central task, arguably the central task, of modelling most combinatorial problems is choosing a representation of complex decision variables. Current finite-domain constraint solvers provide decision variables whose domains contain atomic elements, which we call atomic variables. 1 Yet, combinatorial problems often require finding a more complex combinatorial structure. For example, the Social Golfers Problem (SGP, see [9] problem 10) requires partitioning a set G of golfers in each week of play. Thus, the goal is to find a multiset of partitions of G, i.e. a multiset of sets of sets of G. Modelling the SGP requires deciding how to represent this complex decision variable as a constrained collection of atomic variables.

In concert with choosing a representation of complex decision variables is the task of representing the constraints of the problem. In its natural form, a combinatorial problem imposes constraints on the combinatorial structure that is sought. These constraints must be "translated" so that they are imposed on the representation of the decision variables.

This paper shows how these two central tasks of modelling can be formalised and automated, and in doing so reports two principal contributions. First, we have designed a language, called ESSENCE, that enables combinatorial problems to be stated at a high level of abstraction. This level of abstraction is a consequence of three features: (1) The language supports a wide range of types (including sets, multisets, relations, functions, partitions) and decision variables can be of these types. (2) All types can be nested to arbitrary depth; for example, a decision variable can be of type set, set of sets, set of set of sets, and so forth. (3) Constraints can contain quantifiers that range over decision variables. For example, if a decision variable X is of type set of sets, a constraint can be of the form ∀x ∈ X.φ. The ESSENCE language is outlined in Sec. 3, though only in enough detail to enable the presentation of our second principal contribution.

1 Some finite-domain constraint solvers support variables whose domain elements are finite sets of atomic elements. Though all aspects of our work have considered this, for the sake of simplicity this paper pretends such variables do not exist.

Our second major contribution is the formulation and automation of a set of rules that can refine constraints on complex variables in an ESSENCE specification into constraints on atomic variables, which is the level of abstraction provided by existing constraint languages and toolkits. Our formal rules are presented in Sec. 4.

An attempt to formulate such a set of refinement rules confronts two primary difficulties and many secondary ones. Before proceeding it is worth considering the primary ones.

The first difficulty arises because expressions, particularly decision variables of non-atomic type, can usually, if not always, be refined in multiple ways. Furthermore, the refinement of an operator depends on how its operands are refined. For example, in refining the constraint S1 = S2, where S1 and S2 are atomic set variables, the treatment of equality is different for every combination of ways that S1 and S2 can be refined. Indeed, it is possible that an operator is inapplicable to certain refinements of its operands.

The second major difficulty arises from arbitrary nesting of types. Refining an operator that is applied to expressions whose types are nested provides the biggest challenge. Consider refining the constraint A = B, where A and B are decision variables of some type τ that is nested arbitrarily deep. The generated constraint must involve all components of both A and B. Since there is no bound on the nesting of τ, this complex constraint would have to be generated through recursive rule applications, none of which can look arbitrarily deep into the nesting of τ. Furthermore, we wish to produce refinements in which A and B do not have the same kind of representation. An especially tricky case is when a quantifier ranges over a decision variable of a nested type, such as ∀x⊆A φ, where A is as above.

Modelling in constraints involves more than just representing decision variables and problem constraints. Constraint models often contain many symmetries, often enormous numbers of them, which result in redundancies in the search space. Expert modellers are able to identify such symmetries and break them, either by introducing symmetry-breaking constraints or using a symmetry-aware search method. It has been argued that detecting symmetries in a model is as hard as graph isomorphism. We maintain that symmetries enter a model from two sources: either a symmetry is inherent to the combinatorial problem or it is introduced by the modelling process. An automated modelling system ought to identify the symmetry that it introduces into a model. Sec. 5 explains how this can be integrated into our architecture for model generation.

Another technique used by expert modellers is to represent a complex decision variable with multiple representations simultaneously and impose channelling constraints to keep the representations consistent with each other [4; 8; 11]. This sometimes yields more propagation, and therefore reduced search, than a single representation. As will be seen, the rules of CONJURE generate models with multiple representations. Sec. 6 explains how our refinement rules can generate the information that is needed to automatically generate Given n, put n integer ticks on a ruler of size m such that all inter-tick distances are unique. Minimise m.

given n: int where n ≥ 0 letting bound be 2n find T icks: set (size n) of 0..bound minimising max(Ticks) such that ∀{i, j}⊆Ticks.∀{k, l}⊆Ticks. {i, j} ̸= {k, l} → |i - j| ̸= |k - l|

the appropriate channelling constraints.

We conjecture that the good models of a problem can be generated automatically by formulating the problem in ESSENCE and then refining the specification using rules of the kind presented in this paper. We have implemented a program, called CONJURE, that currently refines a subset of ESSENCE, called mini-ESSENCE. This gives us a platform with which we have experimentally tested our conjecture, as reported in in Sec. 7.

3 An Introduction to ESSENCE

This section briefly introduces the abstract specification language ESSENCE. It is an evolving and growing language; version 1.0 is used within this paper. A full specification of the language can be found at www.cs.york.ac.uk/aig/constraints/AutoModel/.

Let us begin by considering the specification of the Golomb Ruler Problem (GRP, problem 6 at www.csplib.org), shown in Fig. 1). A specification is a list of statements, of which there are seven kinds, signalled by the keywords given, where, letting, find, maximising, minimising and such that. Statements are composed into specifications according to the regular expression

(given | letting | where)∗ find+ [minimising | maximising] (such that)∗

Identifiers in CONJURE come in four categories: constant, parameter, quantified variable, and decision variable. "Letting" statements declare constant symbols and give their values. "Given" statements declare the problem's parameters; the values of the parameters are provided to specify the instance of the problem class. Parameter values are not part of the problem specification; as in other modelling languages, they are provided elsewhere. "Where" statements impose restrictions on the parameter values; only parameter values meeting the restrictions specify a problem instance. "Find" statements declare decision variables. A "minimising" or "maximising" statement gives the objective function, if any. Finally, "such that" statements give the problem's constraints.

The GRP specification begins by declaring n to be a parameter, restricting it to be non-negative and declaring bound to be a constant. Since n is used in the declaration of bound, the declaration of bound must come after the declaration of n. Every symbol must be defined before it is used. This restriction prevents cyclical definitions and means that decision variables cannot be used in the definitions of constants and parameters.

The specification language is strongly typed and every expression and subexpression has a type. The type of the decision variable T icks indicates that the goal of the problem is to find a set containing n elements, each of which is an integer in the range 0 to bound. The types supported by ESSENCE include the atomic types int (integer), bool (Boolean) and l..u (an integer range type), where l and u are integer expressions. ESSENCE also provides enumerated types and a new and very useful atomic type: type (size α), a type of α unnamed elements.

ESSENCE is the first constraint language to support fullycompositional type constructors. So, for example, a decision variable may be of type integer, set of integer, set of set of integer, and so forth. If τ is a type, α is an integer expression, and I1, . . . , In are expressions of type range then the following are types that appear in this paper:

Also among the types of ESSENCE are relations between any two types, partial and total functions from any type to any type, partitions of a set of any type and permutations of any type.

Constraints in this specification language are built from the parameters, constants and decision variables using operators commonly found in mathematics and in other constraint specification languages. The language also includes variable binders such as ∀x, ∃x and ∑x , where x can range over any specified finite type (e.g., integer range but not integer). The constraint in the GRP can be paraphrased as "For any unordered pair {i, j} of ticks and any unordered pair {k, l} of ticks, if the two pairs are different then the distance between i and j is not the same as the distance between k and l." To clarify the notation, the expression {i, j} ⊆ T icks means that two distinct elements are drawn from T icks and, without loss of generality, one is called i and the other is called j.

Now consider the specification of the Sonet problem shown in Fig. 2. Notice that Nodes is declared to be a range. A subtle point is that the third line of the specification is declaring two parameters. When the demand parameter is instantiated to a particular set of sets, the size of the outer set will be known. Hence, the value of m is given indirectly. This declaration also requires the inner sets to have cardinality two. The goal is to find a multiset (representing the rings), each element of which is a set of Nodes (representing the nodes on that ring). The objective is to minimise the sum of the number of nodes installed on each ring. The constraint ensures that any pair of nodes that must communicate are installed on a common ring.

The Target Language: ESSENCE′

ESSENCE specifications are refined into a target language called ESSENCE′ , which is a subset of ESSENCE with a level of abstraction similar to that of existing constraint languages, OPL [19] being the closest. The only types ESSENCE′ has are integers, integer ranges, Booleans and matrices; it does not have enumerated types or types of unnamed elements. Binders, such as quantifiers and summations, range only over integer ranges. From this generic constraint language, it is A Sonet communication network comprises a number of rings, each joining a number of nodes. A node is installed on a ring using an ADM and there is a capacity bound on the number of nodes that can be installed on a ring. Each node can be installed on more than one ring. Communication can be routed between a pair of nodes only if both are installed on a common ring. Given the capacity bound and a specification of which pairs of nodes must communicate, allocate a set of nodes to each ring so that the given communication demands are met. The objective is to minimise the number of ADMs used. (This is a common simplification of the full Sonet problem, as described in [8])

given nrings:int, nnodes:int, capacity:int where nrings≥ 1, nnodes≥ 1, capacity≥ 1 letting Nodes be 1..nnodes given demand:set (size m) of set (size 2) of Nodes find rings: mset (size nrings) of set (maxsize capacity) of Nodes minimising ∑r∈rings |r| such that ∀pair∈demand. ∃r∈rings . pair ⊆ r

a short step to an established constraint language, such as OPL, Solver, or Eclipse. To perform this step, we are developing a suite of back-end translators. In future, we also intend to translate to more restricted languages, such as SAT and Pseudo-Boolean formulations.

4 The Architecture of CONJURE

This section discusses the refinement rules CONJURE uses to refine an ESSENCE expression into a set of ESSENCE′ expressions. For concision we give only a small subset of all the refinement rules 2 ; the remainder follow a similar pattern.

Refining a Simple ESSENCE Specification

Refinement of an ESSENCE specification begins by refining each constraint and the objective function in turn. Let us begin by considering the single-constraint MicroSonet1 specification (Fig. 3), where the goal is to fill two rings with the same nodes.

A key consideration in refining MicroSonet1 is the representation of each ring, each of which is a fixed-size set. This paper uses two representations of fixed-size sets. The explicit representation is a one-dimensional matrix of Nodes indexed by 1..capacity. Each element of the matrix corresponds to an element of the set. To represent the set properly, the elements of the matrix are constrained to take distinct values. The occurrence representation is a one-dimensional Boolean matrix indexed by Nodes, where a true entry indicates that the corresponding node is in the set. To represent the set properly, the number of true entries must be equal to capacity (for counting we treat true/false as 1/0). Fig. 3 gives ESSENCE′ models using both representations. Note that some symbols of ESSENCE, such as "∀" and "Σ", can also be written textually, such as "forall" and "sum". In writing ESSENCE′ we use the textual version.

The refinement operator, ρ, is a function that maps every ESSENCE expression to a set of ESSENCE′ expressions. As explained later, each of these ESSENCE′ expressions is tagged with further information necessary to construct the

2 See http://www.cs.york.ac.uk/aig/constraints/AutoModel/ for the complete set.

given

where

letting

find nnodes : int, capacity : int nnodes ≥ 1, capacity ≥ 1

Nodes be 1..nnodes

ring1 :set(size capacity) of Nodes

ring2 :set(size capacity) of Nodes

such that ring1 = ring2

given

where nnodes:int, capacity:int nnodes ≥ 1, capacity ≥ 1

letting Nodes be 1..nnodes

find ring′1 :matrix [indexed by 1.. capacity] of Nodes ring′2 :matrix [indexed by 1.. capacity] of Nodes

such that forall (i :1..capacity) exists (j :1..capacity) ring′1 [i] = ring′2 [j] AllDifferent(ring′1 )

AllDifferent(ring′2 )

given

where

letting

find nnodes:int, capacity:int nnodes ≥ 1, capacity ≥ 1

Nodes be 1..nnodes

ring′1 :matrix [indexed by Nodes] of bool

ring′2 :matrix [indexed by Nodes] of bool

such that forall (i :Nodes) ring′1 [i]= ring′2 [i]

sum (i : Nodes) ring′1 [i]= capacity

sum (i : Nodes) ring′2 [i]= capacity

Figure 3: ESSENCE specification and two ESSENCE′ models of the MicroSonet1 problem.

final model. ρ is defined inductively by a set of uniquelynamed equations of the form R ρ(e) = e′1 ∪ e′2 ∪ · · · ∪ e′n, where R is the name of the equation, e is an ESSENCE expression and each e′i is a set of ESSENCE′ expressions, usually given via set comprehension. For perspicuity, each equation is split into rules, written: R1 ρ(e) ref→ e′1 , R2 ρ(e) ref→ e′2 , . . ., Rn ρ(e) ref→ e′n.

The SIZEDSETEQUALITY equation is responsible for refining expressions of the form S1 = S2, where both S1 and S2 are expressions of type fixed-size set. Fig. 4 gives two rules of this equation. The complete version of SIZEDSETEQUALITY gives one rule for for each combination of a representation of S1 and a representation of S2 and a constraint for imposing equality between the them.

To illustrate the operation of a rule, we now discuss how the SIZEDSETEQUALITY1 rule refines ring1 = ring2. SIZEDSETEQUALITY1 refines S1 and S2 into explicit onedimensional matrices denoted by S ′1 and S ′2 . The SIZEDSETEQUALITY2 rule proceeds similarly. The reader may wonder at the strategy of refining the arguments of the equality constraint inside the equality rule itself. This is explained in the next sub-section.

When a rule needs to introduce a new identifier, such as that denoted by S ′1 , it does so by making use of the genSymbol function. This function takes two arguments. The first is either an explicit category (see Sec. 3), or an identifier from which the category information is copied. The second is the type of the new identifier, such as a one-dimensional matrix used for the explicit representation. The genSymbol function creates a new identifier of the required category and type that appears nowhere else in the ESSENCE′ model being constructed. When, for example, refining ring1 with SIZEDSETEQUALITY1, S ′1 = genSymbol(ring1 , matrix [indexed by Nodes] of 1..n), and so S ′1 will denote a unique identifier for a matrix of decision variables (since ring1 is a decision variable).

Definitions via genSymbol and type information (except for the input expression) are given on the right of the long vertical bar. The bar itself has no meaning beyond separating the details of the rule from the types and definitions.

Since SIZEDSETEQUALITY1 chooses to represent both sets explicitly, the expression e ="(∀i∃jS ′1[i] = S ′2[j]) ∧ (n1 = n2)" is used to constrain the two explicit matrices to represent the same set (note the introduction of the quantified variables denoted by i and j). Since, in general, it may be the case that e is not yet in ESSENCE′ , it is refined further and the result, denoted by φ, is returned. In this example, e = "∀i ∃j ring′1 [i] = ring′2 [j] ∧ (capacity = capacity)" is in ESSENCE′ , so ρ(e) = e. For brevity, the model shown in Fig. 3 omits capacity = capacity; a simplifier could easily remove it. This convention is followed in all subsequent models generated by SIZEDSETEQUALITY1.

Recall that the explicit representation of a set(size n) of τ is a matrix of n distinct elements, each of type τ. Thus, when a rule generates this explicit representation, it must introduce into the generated model a constraint that the elements of the matrix are all different. In particular, the SIZEDSETEQUALITY1 rule must introduce two such constraints: AllDifferent(S ′1) and AllDifferent(S ′2). And, since the elements of S ′1 and S ′2 have not been refined, ρ must be applied to these two constraints, resulting in the ESSENCE′ constraints named χ and ψ in the rule.

Consider where χ and ψ should occur in the generated model. From the ESSENCE′ model of Fig. 3 it might appear that χ and ψ should be conjoined to φ, returning φ ∧ χ ∧ ψ. To see that this is incorrect, observe that this treatment would refine ¬(ring1 = ring2) to ¬(φ ∧ χ ∧ ψ), whereas the desired refinement is (¬φ) ∧ χ ∧ ψ. The correct refinement is obtained by returning φ as the refinement, tagging the refinement with χ∧ψ, and once the ESSENCE′ model is generated, adding χ ∧ ψ to its constraints. Since, in this case, the tag is a constraint, it is labelled by such that.

When a rule builds a refinement R, a part P of which has been generated from a recursive call to ρ, the tags of P are, by default, added to the tags of R. Hence, in SIZEDSETEQUALITY1, the tags attached to a refinement of φ, χ and ψ are implicitly added to the such that tag explicitly given in the rule. As will be seen later, this default can be overridden.

Space precludes giving the full derivation of the explicit ESSENCE′ model (Fig. 3). The refinements triggered via SIZEDSETEQUALITY1 in the example are, however, straightforward. Universal quantification over a finite range of integers is in ESSENCE′ and can be viewed as a conjunction or simple 'for' loop. Similarly, existential quantification over a finite range of integers can be treated as disjunction. Hence, the first constraint in the explicit ESSENCE′ model comes directly from SIZEDSETEQUALITY1. The occurrence model follows similarly.

After refining the constraints and the objective function of an ESSENCE specification, the given find and letting statements are generated. This is done by scanning the set of constraints and adding an appropriate definition for each unique identifier. where statements are refined in the same

SizedSetEquality1 ρ(S1 : set (size n1) of τ = S2 : set (size n2) of τ) ref→ { φsuch that χ∧ψ |φ ∈ ρ((∀i∃jS′1 [i] = S′2 [j]) ∧ (n1 = n2)) χ ∈ ρ(AllDifferent(S′1 )) ψ ∈ ρ(AllDifferent(S′2 )) } S′1 =genSymbol(S1, matrix [indexed by 1..n1] of τ) S′2 =genSymbol(S2, matrix [indexed by 1..n2] of τ) i = genSymbol("Quantified variable", 1..n1) j = genSymbol("Quantified variable", 1..n2) SizedSetEquality2 ρ(S1 : set (size n1) of τ = S2 : set (size n2) of τ) ref→ { φsuch that χ∧ψ |φ ∈ ρ((∀iS′1 [i] = S′2 [i]) ∧ (n1 = n2)) χ ∈ ρ(ΣiS′1 [i] = n1) ψ ∈ ρ(ΣiS′2 [i] = n2) } τ is [a..b] or bool S′1 = genSymbol(S1, matrix [indexed by τ] of bool) S′2 = genSymbol(S2, matrix [indexed by τ] of bool) i = genSymbol("Quantified variable", τ ) ForallRange1 ρ(∀i :n1..n2 φ:bool) ref→ { forall (i :n1..n2) φ′ such that forall (i :n1..n2) Γ |(φ′ with such that Γ) ∈ ρ(φ) } ForallSizedSet1 ρ(∀i : τ ∈ S : set (size n) of τ.φ : bool) ref→ { forall (j :1..n) φ′ such that χ∧ forall (j :1..n) Γ |(φ′ with such that Γ) ∈ ρ(φ[i ↦→ S′ [j]]) χ ∈ ρ(AllDifferent(S′ )) } j = genSymbol(i, 1..n) S′ = genSymbol(S,matrix [indexed by 1..n] of τ) SizedSubset1 ρ(S1 : set (size n1) of τ ⊆ S2 : set (size n2) of τ) ref→ { φsuch that χ∧ψ |φ ∈ ρ(∀i.S′2 [S′1 [i]]) χ ∈ ρ(ΣjS′2 [j] = n2) ψ ∈ ρ(AllDifferent(S′1 )) } τ is [a..b] or bool S′1 = genSymbol(S1, matrix [indexed by 1..n1] of τ) S′2 = genSymbol(S2, matrix [indexed by τ] of bool) i = genSymbol("Quantified variable", 1..n1) j = genSymbol("Quantified variable", τ )

way that constraints are.

Refining Nested Types: A Simple Example

To see how expressions of a nested type are refined, consider the Microsonet2 specification (Fig. 5), where the goal is to generate two identical sets of rings. The key decision is the representation of rings1 and rings2, two sets of sets. Refinement begins with ρ(rings1 = rings2), requiring SIZEDSETEQUALITY. Of the rules given in Fig. 4, only SIZEDSETEQUALITY1 is applicable, since "set (size capacity) of Nodes" is neither a range of integers nor Boolean: indexing a matrix by a complex type (here each index would correspond to one of the possible sets of Nodes) would often lead to unfeasibly large matrices. Future work will consider relaxing this condition in certain cases.

The justification for refining the arguments of the equality constraint inside the equality rule itself becomes clear in the context of nested types. A seemingly more-natural approach to refining S1 = S2 would be to refine S1 and S2 and constrain the results to be equal. However, given unbounded nesting of types and multiple possible refinements of each type, constraining the results to be equal is not straightforward. Consider the case where S1 and S2 are not sets of integers, but sets of sets of . . . sets of integers. Having refined S1 and S2 there is no fixed constraint on their refinements that enforces equality on S1 and S2. Instead of this approach, our rules are designed to "peel off" a layer of nesting so that the associated constraint/operator can be formed without looking arbitrarily deep inside a refined expression.

Performing SIZEDSETEQUALITY1 requires refining the two such that tags, both of which impose that all the elements of a matrix of sets must be different. Since these elements may be of a non-atomic type, this AllDifferent constraint must be refined. For space reasons the definition of the ALLDIFFERENT refinement rules are omitted.

The main constraint generated by SIZEDSETEQUALITY1 is ρ(∀i∃jrings′1 [i] = rings′2 [j]). The FORALLRANGE equation is now applicable (Fig. 4 gives FORALLRANGE1). This rule works by refining φ, which contains the free variable i. Each resulting refinement φ′ and its tag Γ, both of which contain the free variable i, are wrapped in "forall i : n1..n2." Refinement continues with ρ(∃j rings′1 [i] = rings′2 [j]). EXISTSRANGE operates in the same way as FORALLRANGE, so we omit the details.

We now have ρ(rings′1 [i] = rings′2 [j]), for which SIZEDSETEQUALITY is used. Both rules are applicable, since rings′1[i] and rings′2[i] are sets of Nodes. The refinement in Fig. 5 uses SIZEDSETEQUALITY2 to generate an occurrence representation of the inner sets. The rule operates as described earlier, but we highlight how genSymbol treats indexed matrices. genSymbol respects the index structure of its first argument. Hence, given the indexed one-dimensional array rings′1[i], genSymbol(rings′1 [i], matrix...) creates a two-dimensional Boolean matrix, rings′′ 1 (see Fig.5), and returns the partially-indexed rings′′ [i], which is the refined version of an element of the set of sets.

The remaining refinements are straightforward. Note that rings′1, rings′2 are not in the model. These are intermediate representations which, although more concrete than rings1

given nrings : int, nnodes : int, capacity : int where nrings ≥ 1, nnodes ≥ 1, capacity ≥ 1 letting Nodes be 1..nnodes find rings1 : set (size nrings) of set (size capacity) of Nodes rings2 : set (size nrings) of set (size capacity) of Nodes such that rings1 = rings2 given nrings:int, nnodes:int, capacity:int where nrings ≥ 1, nnodes ≥ 1, capacity ≥ 1 letting Nodes be 1..nnodes find rings′′ 1 :matrix [indexed by 1..nrings, Nodes] of bool rings′′ 2 :matrix [indexed by 1..nrings, Nodes] of bool such that forall (i :1..nrings) exists (j :1..nrings) forall (k:Nodes) rings′′ 1 [i][k] = rings′′ 2 [j][k] forall (i :1..nrings) sum (j :Nodes) (rings′′ 1 [i][j]) = capacity forall (i :1..nrings) sum (j :Nodes) (rings′′ 2 [i][j]) = capacity forall (i, j :1..nrings) i<j implies exists (k:Nodes) rings′′ 1 [i][k] ̸= rings′′ 1 [j][k] forall (i, j :1..nrings) i<j implies exists (k:Nodes) rings′′ 2 [i][k] ̸= rings′′ 2 [j][k]

given nrings : int, nnodes : int, capacity : int where nrings ≥ 1, nnodes ≥ 1, capacity ≥ 1 letting Nodes be 1..nnodes given demand : set (size m) of set (size 2) of Nodes find rings : set (size nrings) of set (size capacity) of Nodes such that ∀pair∈demand. ∃r∈rings . pair ⊆ r given nrings:int, nnodes:int, capacity:int where nrings ≥ 1, nnodes ≥ 1, capacity ≥ 1 letting Nodes be 1..nnodes given demand ′′ :matrix [indexed by 1..m, 1..2] of Nodes find rings′′ :matrix [indexed by 1..nrings, Nodes] of bool such that forall (i :1..m) exists (j :1..nrings) forall (k:1..2) rings′′ [j][demand′′ [i][k]] forall (i :1..nrings) sum (j :Nodes) (rings′′ [i][j]) = capacity forall (i, j :1..nrings) i<j implies exists (k :Nodes) rings′′ [i][k] ̸= rings′′ [j][k]

and rings2, are matrices of sets, and so not in ESSENCE′ .

Refining Nested Types: A Complex Example

Our final example illustrates a difficult case when refining nested types: quantification over nested types. Consider MicroSonet3 (Fig. 6), a variant of a large piece of SONET, where the goal is to fill a given number of rings such that the inter-node communication demand is met. Refinement begins with ρ(∀pair ∈ demand.∃r ∈ rings.pair ⊆ r), using the FORALLSIZEDSET1 rule (Fig. 4). The first step is to refine the binding expression, pair ∈ demand, which is, in turn, dependent on the refinement of the given set demand. FORALLSIZEDSET1 represents demand explicitly in the same way as SIZEDSETEQUALITY1. The returned expression quantifies over the indices of this matrix.

The quantified expression φ (which is ∃r ∈ rings.pair ⊆ r in the example) is refined in the context of the decision to represent the set S explicitly as the matrix S ′ . In doing so, S ′ [j] is substituted for i via φ[i ↦→ S ′ [j]] (in the example demand′ [j] is substituted for pair). As per FORALLRANGE1, the tags associated with this refinement must also be quantified to hold for each possible value of j. Having highlighted this case, space precludes giving further details of the refinement. One particular rule, SIZEDSUBSET1, which is central to this specification, is presented in Fig. 4. This rule shows two expressions, S1 and S2, of the same type being refined to two different representations. The design of CONJURE means this is no more complicated than the previously presented rules, which produce identical representations.

Refining Nested Operators

None of the refinement examples considered so far have used an ESSENCE specification with nested operators. We have avoided the extremely difficult task of formulating refinement rules that recur on both the type of an expression and its syntactic structure. Each recursive rule either works recursively on syntactic structure and handles only atomic types or it works recursively on nested types and handles only expressions that are syntactically "primitive" (in a sense not defined here). A constraint containing both nested types and nonprimitive syntactic structure is refined by first rewriting it to an equivalent one containing only primitive syntactic structure. For example, the constraint A∩(B∪C) ⊆ D is rewritten to ∃X, Y (X= B∪C) ∧ (Y =A∩X) ∧ (X ⊆D). Each conjunct of the resulting constraint is a primitive constraint that has a dedicated refinement rule. CONJURE performs this rewriting in a preprocessing stage called flattening.

5 Some Symmetry Detection is Free

Refinement often introduces symmetries into the models it generates; that is, the generated model contains symmetries that do not correspond to symmetries in the original specification. This always happens when a variable X in the specification is represented by a collection of variables X ′1 , . . . , X ′n in the model such that an instantiation of X corresponds to multiple instantiations of X ′1 , . . . ,X ′n. For example, if X is of type set (size 3), its explicit representation is a matrix of three variables, X ′ [1..3]. An instantiation of X corresponds to 3! instantiations of X ′ [1..3]. The matrix X ′ has index symmetry [6], which can broken by the symmetry-breaking constraint X ′ [1] ≤ X ′ [2] ≤ X ′ [3].

Since certain rules always introduce symmetry, such a rule can tag the refined expression with a description of the symmetry. For example, (though not shown in Fig. 4) SIZEDSETEQUALITY1 tags φ with "symmetry indexsym(φ, 1)," which indicates that φ has symmetry in its first index. Once a model has been generated, the symmetry tags can be used to add appropriate symmetry-breaking constraints, or to guide a symmetry-aware search method such as SBDS or SBDD.

Detecting symmetry as refinement introduces it is a considerably cheaper operation than symmetry detection on a finished model. In future, we intend to extend our system of symmetry tags to include other types of symmetry, such as partial index symmetry and value symmetry.

6 Generating Models with Channelling

As we have seen, ESSENCE expressions have multiple possible refinements. If the same expression appears multiple times in a specification, then, different refinements of it may appear in an ESSENCE′ model. Sometimes these concrete representations have a different name but they are equivalent. In those cases CONJURE automatically unifies them into a single representation. However, CONJURE often produces distinct concrete representations for the same abstract symbol. At first sight, this may appear to be a weakness. On the contrary, some of the most effective models in the literature take this approach, since some representations allow certain constraints to be modelled more easily than others. To maintain consistency among the different representations, channelling constraints are used [4].

To facilitate channelling, (though not shown in Fig 4) the refinement rules add represent tags to the refinements to record the relationship between ESSENCE identifiers and their representations in the concrete model. For example, when refining a decision variable S of type set (size n) of int it is possible for S to be represented by both occurrence and explicit representations in the same model. If that is the case the model will contain the tags "represent S by expset(S1)" and "represent S by occset(S2)," connecting S with its concrete representations S1 and S2. By following the chain of tags it is possible to connect each concrete object to the original entity it is representing, and from these it is possible to construct channelling constraints.

7 Experimental Results

This paper makes an empirically testable conjecture: it is possible to develop good constraint models for combinatorial problems by specifying the problem in ESSENCE and refining this specification with CONJURE. At this point we can test the conjecture up to certain limits. The first limitation is that we currently are concerned only with the kernel of the model, which lacks channelling constraints and symmetry-breaking constraints and which has not had any transformations applied. The second limitation is that the implementation of CONJURE currently has rules for only certain types: integers, integer ranges, Booleans, bounded and fixed-size sets, bounded and fixed-size multisets, and all compositions of these. The implemented rules can generate ESSENCE′ models with occurrence and explicit representations and with variables whose domains contain sets of integers.

We test this conjecture by identifying problems that can be specified using only the supported types, and checking whether CONJURE generates the kernel of all reasonable models, particularly models appearing in the literature. Most problems in the literature cannot be specified abstractly with the supported types since they involve associating together elements from two or more sets, which requires types such as functions or relations. We have found seven problems in the literature that can be specified abstractly with only the supported types: Schur's Lemma (SL), Balanced Incomplete Block Design (BIBD), Steiner Triple Systems (STS), SONET (SONET), Social Golfers Problem (SGP), RL Design (RLD), and Balance Code Generation (BCG). Though we know of no published models for RLD and BCG (both come from [5]), we have included them simply to test whether CONJURE can generate reasonable, correct models.

The results of running CONJURE on ESSENCE specifications of these seven problems are summarised in the Table 1.

To see how to interpret the table, consider the row labelled SONET. This indicates that CONJURE generated 27 models for this problem. The choices it had to make were how to represent each of the two occurrences of the decision variable (whose type is set of set) and the one occurrence of the input parameter (whose type is set of sets). Our survey of the literature uncovered four published models (all in [8]) that were among those generated by CONJURE and four (all in [8]) that were not. The entry for SGP indicates that CONJURE generated two of the three models that we found in the literature. Though some models appear in multiple published papers, the table cites only one.

Examining the results of the experiments, we observed that all of the models generated by CONJURE were correct. The kernels of many models found in the literature were generated by CONJURE; that is, the models use the same decision variables and the same problem constraints (as opposed to implied or channelling constraints).

It is more enlightening to consider the models not generated by CONJURE. The four models of SONET not generated by CONJURE arise straightforwardly by considering the decision variable to be a relation between rings and nodes. The rules for refining a relation in this way could be expressed easily in the framework of CONJURE and would enable the generation of these four additional models. This illustrates that there are important issues involved in writing specifications in ESSENCE, which in this case are also intertwined with the detection of symmetry; all of this is outside the scope of this paper.

The missing model of SL could be generated easily from the most natural expression of the problem, which takes the decision variable to be a partition. Again, it would be straightforward to add to CONJURE the necessary rules for partitions.

Finally, the model of SGP not generated by CONJURE uses a novel modelling technique that was created through insight into the structure of the problem. We have not yet considered whether that technique can be generalised and then captured in CONJURE rules.

8 RelatedWork inModelling Support

OPL [19], a modelling language similar to ESSENCE′ , has been extended by ESRA [7] to provide relation variables and by F [11] to provide function variables. ESRA currently compiles to only a single representation, but F can produce alternative models, some with multiple representations and channelling. Other work has extended constraint languages to support a single representation of both sets [10] and multisets [20]. However our work is unique in providing nested types.

Other languages have been used to specify combinatorial problems. NP-SPEC [3] uses existential second-order logic to express executable specifications of every NP-complete problem. Renker et al. [15] discuss representing abstract specifications in Z, an expressive abstract language that is supported by automatic type-checkers and interactive tools. However, refinement and transformation of the Z specification is manual.

Multi-tac [14] and CACP [2; 1] are systems that perform small-scale transformations of constraint specifications and use heuristics and search to try to improve the search strategy used in the solving of CSPs. These and similar systems are important steps towards automating the solving of CSPs, and complement our work on CONJURE, which at present is only concerned with refining of high-level specifications and not the search strategy to be used, and does not implement transformation rules as of yet.

The area of automatic program refinement is a longstanding and mature area of computer science. KIDS [17] and Specware [18] are among the many domain-independent systems that support the interactive or automatic refinement of formal specifications into imperative programs. Our work on CONJURE operates in a simpler setting of transforming specifications into finite-domain constraint models, which are declarative. Because our setting is simpler, we can be more ambitious about the extent of automation achieved.

9 Conclusion

This paper has made two major contributions towards realising the possibility of formalising and automating the generation of constraint models. First, the paper has presented a language that enables combinatorial problems to be specified at a level above that at which modelling decisions take place. Second, the paper has shown how a system of formal rules could refine such a specification into model kernels at the level of abstraction supported by existing constraint solvers. We have also outlined an approach to integrating other aspects of model generation-channelling and symmetry breaking-into the existing system.

A rigorous account of model generation would be valuable in several ways. It could make our study of modelling more systematic, revealing gaps in our understanding. It could also guide the study of model selection by identifying the decision points and the set of alternatives available at each. Furthermore, it would be useful in teaching and presenting modelling and in constructing a catalogue of modelling constructs.

The automation of model generation offers further opportunities. CONJURE currently uses its rules to generate all possible models; but the rules could also be used within an interactive system, which, like an interactive theorem prover, allows the user to chose from among the alternatives available at a decision point. Our ultimate dream is that the automation of model generation takes us one step closer to automating the entire modelling process.

Acknowledgements Ian Miguel is supported by a UK-Royal Academy of Engineering/EPSRC Postdoctoral Fellowship. We thank Adam Bakewell for contributing to an early version of this work, and Brahim Hnich and Toby Walsh for useful discussions.