Towards the Systematic Generation of Channelling Constraints

The automatic modelling tool

Conjure

[1] generates CSP models from a problem specified in the specification language

Essence

. Variables in

Essence

may have domains currently unsupported by solvers. Also, the elements of the domains may be arbitrarily compound, for example, sets of sets, sets of sets of sets.

Conjure

uses a set of

refinement rules

to compositionally transform the variables (and constraints) into representations that can be implemented in current solvers.

Conjure

can produce multiple alternative (redundant) representations of the same variable that may appear simultaneously in the same model. Currently,

Conjure

does not generate the

channelling constraints

[2] that are needed to maintain the consistency between these simultaneous alternatives.

There are several unsolved issues related to channeling constraints and automatic modelling, such as, how to identify the cases where a channelled model performs better than a non-channelled one, and how to implement the channelling constraints efficiently. In this paper however, we focus the automated generation of channelling constraints under the

Conjure

framework.

Our work has identified and proved correct, an algorithm to systematically generate the channelling constraints needed in a

Conjure

-generated model. We briefly describe this algorithm as follows. Let

P

be a specification refined by

Conjure

into the CSP model

P

′. Let

X

be a variable in

P

that has two representations

X

1

and

X

2

in

P

′. Let

Y

be a new variable with exactly the same domain of

X

. We can then

re-refineX

=

Y

(channelling constraint between

X

and

Y

)

forcing

the

X

to refine into

X

1

and the

Y

into

X

2

. Hence, we produce a correct channelling constraint between

X

1

and

X

2

providing

Conjure

generates correct refinements.