4.5.1. Prolog facts describing a constraint
For each global constraint, the electronic version of its description is provided as a Prolog file (see the link “.pl file” at the beginning of the section corresponding to a global constraint). In addition the file “eval.pl” contains a set of shared utilities used for evaluating the constraints. This electronic version was used for generating the LaTeX file of this catalogue, the figures associated with the graph-based description and a filtering algorithm for some of the constraints that use the automaton-based description. Within the electronic version, each constraint is described in terms of meta-data. A typical entry is:
ctr_date(minimum, ['20000128','20030820','20040530',
'20041230','20060811','20090416']).
ctr_origin(minimum, '\\index{CHIP|indexuse}CHIP', []).
ctr_arguments(minimum, ['MIN'-dvar, 'VARIABLES'-collection(var-dvar)]).
ctr_exchangeable(minimum,
[items('VARIABLES',all),
vals(['VARIABLES'^var],int,=\=,all,in),
translate(['MIN','VARIABLES'^var])]).
ctr_synonyms(minimum, [min]).
ctr_restrictions(minimum, [size('VARIABLES')>0, required('VARIABLES',var)]).
ctr_typical(minimum, [size('VARIABLES') > 1, range('VARIABLES'^var) > 1]).
ctr_pure_functional_dependency(minimum, []).
ctr_functional_dependency(minimum, 1, [2]).
ctr_aggregate(minimum, [], [min, union]).
ctr_graph(minimum,
['VARIABLES'],
2,
['CLIQUE'>>collection(variables1,variables2)],
[variables1^key=variables2^key #\/ variables1^var<variables2^var],
['ORDER'(0,'MAXINT',var)='MIN'],
[]).
ctr_example(minimum,
[minimum(2,[[var-3],[var-2],[var-7],[var-2],[var-6]]),
minimum(7,[[var-8],[var-8],[var-7],[var-8],[var-7]])]).
ctr_cond_imply(minimum, deepest_valley,
[first('VARIABLES'^var) > 'MIN',
last('VARIABLES'^var) > 'MIN'], [], id).
ctr_see_also(minimum,
[link('generalisation', minimum_modulo,
'%e replaced by %e', [variable, variable mod constant]),
link('specialisation', min_n,
'minimum or order %e replaced by absolute minimum', [n]),
link('comparison swapped', maximum, '', []),
link('common keyword', maximum, '%k', ['order constraint']),
link('soft variant', open_minimum, '%k', ['open constraint']),
link('soft variant', minimum_except_0, 'value %e is ignored', [0]),
link('implies', between_min_max, '', []),
link('implies', in, '', []),
link('implied by', and, '', [])]).
ctr_key_words(minimum,['order constraint' ,
'minimum' ,
'maxint' ,
'automaton' ,
'automaton without counters' ,
'reified automaton constraint' ,
'centered cyclic(1) constraint network(1)',
'arc-consistency' ]).
ctr_persons(minimum,['Beldiceanu N.']).
ctr_eval(minimum, [builtin(minimum_b), automaton(minimum_a)]).
minimum_b(MIN, VARIABLES) :-
check_type(dvar, MIN), collection(VARIABLES, [dvar]),
length(VARIABLES, N), N > 0,
get_attr1(VARIABLES, VARS), minimum(MIN, VARS).
minimum_a(MIN, VARIABLES) :- % 0: MIN<VAR, 1: MIN=VAR, 2: MIN>VAR
minimum_signature(VARIABLES, SIGNATURE, MIN),
automaton(SIGNATURE, _, SIGNATURE,
[source(s),sink(t)],
[arc(s,0,s),arc(s,1,t),arc(t,1,t),arc(t,0,t)],
[],[],[]).
minimum_signature([], [], _).
minimum_signature([[var-VAR]|VARs], [S|Ss], MIN) :-
S in 0..2,
MIN #< VAR #<=> S #= 0, MIN #= VAR #<=> S #= 1, MIN #> VAR #<=> S #= 2,
minimum_signature(VARs, Ss, MIN).
ctr_sol(minimum,2,0,2,9,[0-5,1-3,2-1]).
ctr_sol(minimum,3,0,3,64,[0-37,1-19,2-7,3-1]).
ctr_sol(minimum,4,0,4,625,[0-369,1-175,2-65,3-15,4-1]).
ctr_sol(minimum,5,0,5,7776,[0-4651,1-2101,2-781,3-211,4-31,5-1]).
ctr_sol(minimum,6,0,6,117649,[0-70993,1-31031,2-11529,3-3367,
4-665,5-63,6-1]).
ctr_sol(minimum,7,0,7,2097152,[0-1273609,1-543607,2-201811,3-61741,
4-14197,5-2059,6-127,7-1]).
ctr_sol(minimum,8,0,8,43046721,[0-26269505,1-11012415,2-4085185,
3-1288991,4-325089,5-58975,6-6305,7-255,
8-1]).
and consists of the following Prolog facts, where is the name of the constraint under consideration. The facts are organised in the following 20 items:
Items 1, 2, 3, 4, 16 and 17 provide general information about a global constraint,
Items 5, 6, 7 and 8 describe the arguments of a global constraint.
Items 9 and 10 give properties of the arguments of a global constraint, e.g. functional dependency, contractibility.
Item 11 describes symmetries of a global constraint, i.e. list of mappings (e.g., permutation of arguments) that preserve the solutions of a global constraint.
Items 12 and 13 describes the meaning of a global constraint in terms of a graph-based representation.
Item 14 provides one or several ground instances which hold.
Item 18 gives the list of available evaluators of a global constraint.
Item 19 provides the number of solutions of the constraint under various assumptions on the number of variables and on their initial domains.
Item 20 describes the meaning of a global constraint in terms of a set of first order logic formulae.
Items 1, 2, 6 and 14 are mandatory, while all other items are optional. We now give the different items:
ctr_date
is a list of dates when the description of the constraint was modified.
ctr_origin
is a string denoting the origin of the constraint. is a possibly empty list of constraint names related to the origin of the constraint.
ctr_usual_name
When, for some reason, the constraint name used in the catalogue does not correspond to the usual name of the constraint, provides the usual name of the constraint. This stems from the fact that each entry of the catalogue should have a distinct name. This is for instance the case for the and the constraints which are both usually called .
ctr_synonyms
ctr_types
is a list of elements of the form -, where is the name of a new type and the type itself (usually a collection). Basic and compound data types were respectively introduced in sections 2.2.1 and 2.2.2 on page 2.2.1. This field is only used when we need to declare a new type that will be used for specifying the type of the arguments of the constraint. This is for instance the case when one argument of the constraint is a collection for which the type of one attribute is also a collection. This is for instance the case for the constraint where the unique argument is a collection of ; refers to a new type declared in .
ctr_arguments
ctr_restrictions
ctr_typical
ctr_pure_functional_dependency
Indicate that, under the assumption that all restrictions described by hold, at least one of the arguments of the constraint is functionally determined by the other arguments. Possible restrictions were described in Section 2.2.3 on page 2.2.3. Which argument is determined by which subset of arguments is described by the fact ctr_functional_dependency where arguments are denoted by their positions within the constraint.
ctr_aggregate
Denotes that, given two instances of the constraint that both satisfy all restrictions described by , we can combine (i.e., aggregate) these two instances in order to obtain an implied constraint, which has the same name as the first two constraints. We use in order to obtain the arguments of the implied constraint as described in the keyword Aggregate.
ctr_exchangeable
ctr_derived_collections
ctr_graph
is a list of collections used for creating the vertices of the initial graph. This was described at page 2.3.3.1 of Section 2.3.3.1.
is the number of vertices of an arc. Arc arity was explained at page 2.3.3.1 of Section 2.3.3.1.
is a list of arc generators. Arc generators were introduced at page 2.3.3.1 of Section 2.3.3.1.
is a list of arc constraints. Arc constraints were defined in Section 2.3.2.2 on page 2.3.2.2.
is a list of graph properties. Graph properties were described in Section 2.3.2.4 on page 2.3.2.4.
ctr_example
is a list of examples (usually one). Each example corresponds to a ground instance for which the constraint holds.
ctr_cond_imply
is a constraint implied by provided that
the list of restrictions holds for the constraint , and
the list of restrictions holds for the constraint .
describes how to create the arguments of from the arguments of . Note that some arguments of may not be explicitly mentioned since they correspond to existentially quantified variables.
ctr_see_also
is a list of constraints that are related in some way to the constraint. Each element of the list is a fact of the form , where:
is a semantic link that explains why we refer to . Semantic links were described in Section 2.6 on page 2.6.
is the name of the constraint that is linked to .
is a string providing contextual explanation.
is a list of symbols (e.g., keywords, constraint names, mathematical expressions) that are inserted in .
ctr_key_words
is a list of keywords associated with the constraint. Keywords may be linked to the meaning of the constraint, to a typical pattern where the constraint can be applied or to a specific problem where the constraint is useful. All keywords used in the catalogue are listed in alphabetic order in Section 3.7 on page 3.7. Each keyword has an entry explaining its meaning and providing the list of global constraints using that keyword.
ctr_eval
For many of the constraints of the catalogue one or several evaluators are provided. Each evaluator is explicitly described in by an element of the form , where is the name of the Prolog predicate to call in order to evaluate the constraint,Note that this predicate name should be different from existing SICStus built-ins, and can be one of the following keywords:
when the corresponding evaluator uses a SICStus built-in. This is for instance the case for the constraint.
when the corresponding evaluator reformulates the constraints in terms of a conjunction of constraints of the catalogue and/or in term of a conjunction of reified constraints. This is for instance the case for the constraint.
when the corresponding evaluator is based on an automaton that describes the set of solutions accepted by the constraint. The evaluator corresponds to the Prolog code that creates the signature constraints as well as the automata (usually one) associated with the constraint. A fact of the form automaton/9 lists the states and the transitions of the automata used for describing the set of solutions accepted by the constraint. It follows the description provided in Section 2.4.2 on page 2.4.2. The constraint is an example of constraint for which an automaton is provided.
when the corresponding evaluator is based on a first order logic formula that describes the meaning of the constraint. This is for instance the case for the constraint.
when the corresponding evaluator only accepts ground instances of the constraint. This is for instance the case for the constraint.
ctr_sol
is the number of variables of the collection of variables.
is the smallest value of the variables of the sequence of variables.
is the largest value of the variables of the sequence of variables.
is the total number of solutions of the constraint, assuming a collection with items and all variables within interval .
is a list, which for each value that can be assigned to an argument of the constraint, gives the corresponding number of solutions assuming we have a collection with items, and that all variables of the collection are assigned a value in interval .
ctr_logic
is a list of first order logical formulae that describe the meaning of the constraint [CarlssonBeldiceanuMartin08].