2.3.1. Selecting an appropriate description

As we previously said, we focus on those global constraints that can be checked by scanning once through their variables. This is for instance the case of:

Since they illustrate key points needed for characterising the set of solutions associated with a global constraint, our discussion will be based on the last five constraints for which we now recall the definition:

Figure 2.3.1. Five checkers and their corresponding automata
ctrs/five_checkers

Parts (A1), (B1), (C1), (D1) and (E1) of Figureย 2.3.1 depict the five checkers respectively associated with ๐š๐š•๐š˜๐š‹๐šŠ๐š•_๐šŒ๐š˜๐š—๐š๐š’๐š๐šž๐š’๐š๐šข, with ๐š•๐šŽ๐šก_๐š•๐šŽ๐šœ๐šœ๐šŽ๐šš, with ๐šŠ๐š–๐š˜๐š—๐š, with ๐š’๐š—๐š๐š•๐šŽ๐šก๐š’๐š˜๐š— and with ๐šŠ๐š•๐š•๐š๐š’๐š๐š๐šŽ๐š›๐šŽ๐š—๐š. For each checker we observe the following facts:

  • Within the checker depicted by partย (A1) of Figureย 2.3.1, the values of the sequence ๐šŸ๐šŠ๐š›๐šœ[0],...,๐šŸ๐šŠ๐š›๐šœ[n-1] are successively compared against 0 and 1 in order to check that we have at most one group of consecutive 1. This can be translated to the automaton depicted by partย (A2) of Figureย 2.3.1. The automaton takes as input the sequence ๐šŸ๐šŠ๐š›๐šœ[0],...,๐šŸ๐šŠ๐š›๐šœ[n-1], and triggers successively a transition for each term of this sequence. Transitions labelled by 0, 1 and $ are respectively associated with the conditions ๐šŸ๐šŠ๐š›๐šœ[i]=0, ๐šŸ๐šŠ๐š›๐šœ[i]=1 and i=n. Transitions leading to failure are systematically skipped. This is why no transition labelled with a 1 starts from state z.

  • Within the checker given by partย (B1) of Figureย 2.3.1, the components of vectors x โ†’ and y โ†’ are scanned in parallel. We first skip all the components that are equal and then perform a final check. This is represented by the automaton depicted by partย (B2) of Figureย 2.3.1. The automaton takes as input the sequence โŒฉx[0],y[0]โŒช,...,โŒฉx[n-1],y[n-1]โŒช and triggers a transition for each term of this sequence. Unlike the ๐š๐š•๐š˜๐š‹๐šŠ๐š•_๐šŒ๐š˜๐š—๐š๐š’๐š๐šž๐š’๐š๐šข constraint, some transitions now correspond to a condition (e.g.,ย x[i]=y[i], x[i]<y[i]) between two variables of the ๐š•๐šŽ๐šก_๐š•๐šŽ๐šœ๐šœ๐šŽ๐šš constraint.

  • Note that the ๐šŠ๐š–๐š˜๐š—๐š(๐š—๐šŸ๐šŠ๐š›, ๐šŸ๐šŠ๐š›๐šœ, ๐šŸ๐šŠ๐š•๐šž๐šŽ๐šœ) constraint involves a variable ๐š—๐šŸ๐šŠ๐š› whose value is computed from a given collection of variables ๐šŸ๐šŠ๐š›๐šœ. The checker depicted by partย (C1) of Figureย 2.3.1 counts the number of variables of ๐šŸ๐šŠ๐š›๐šœ[0],...,๐šŸ๐šŠ๐š›๐šœ[n-1] that take their value in ๐šŸ๐šŠ๐š•๐šž๐šŽ๐šœ. For this purpose it uses a counter c, which is eventually tested against the value of ๐š—๐šŸ๐šŠ๐š›. This convinced us to allow the use of counters in an automaton. Each counter has an initial value, which can be updated while triggering certain transitions. The final state of an automaton can force a variable of the constraint to be equal to a given counter. Partย (C2) of Figureย 2.3.1 describes the automaton corresponding to the code given in partย (C1) of the same figure. The automaton uses the counter variable c initially set to 0 and takes as input the sequence ๐šŸ๐šŠ๐š›๐šœ[0],...,๐šŸ๐šŠ๐š›๐šœ[n-1]. It triggers a transition for each variable of this sequence and increments c when the corresponding variable takes its value in ๐šŸ๐šŠ๐š•๐šž๐šŽ๐šœ. The final state returns a success when the value of c is equal to ๐š—๐šŸ๐šŠ๐š›. At this point we want to stress the following fact: it would have been possible to use an automaton that avoids the use of counters. However, this automaton would depend on the effective value of the argument ๐š—๐šŸ๐šŠ๐š›. In addition, it would require more states than the automaton of partย (C2) of Figureย 2.3.1. This is typically a problem if we want to have a fixed number of states in order to save memory as well as time.

  • As the ๐šŠ๐š–๐š˜๐š—๐š constraint, the ๐š’๐š—๐š๐š•๐šŽ๐šก๐š’๐š˜๐š—(๐š—๐š’๐š—๐š,๐šŸ๐šŠ๐š›๐šœ) constraint involves a variable ๐š—๐š’๐š—๐š whose value is computed from a given sequence of variables ๐šŸ๐šŠ๐š›๐šœ[0], ..., ๐šŸ๐šŠ๐š›๐šœ[n-1]. Therefore, the checker depicted in partย (D1) of Figureย 2.3.1 uses also a counter c for counting the number of inflexions, and compares its final value to the ๐š—๐š’๐š—๐š argument. The automaton depicted by partย (D2) of Figureย 2.3.1 represents this program. It takes as input the sequence of pairs โŒฉ๐šŸ๐šŠ๐š›๐šœ[0],๐šŸ๐šŠ๐š›๐šœ[1]โŒช, โŒฉ๐šŸ๐šŠ๐š›๐šœ[1],๐šŸ๐šŠ๐š›๐šœ[2]โŒช ,..., โŒฉ๐šŸ๐šŠ๐š›๐šœ[n-2],๐šŸ๐šŠ๐š›๐šœ[n-1]โŒช and triggers a transition for each pair. Note that a given variable may occur in more than one pair. Each transition compares the respective values of two consecutive variables of ๐šŸ๐šŠ๐š›๐šœ[0..n-1] and increments the counter c when a new inflexion is detected. The final state returns a success when the value of c is equal to ๐š—๐š’๐š—๐š.

  • The checker associated with ๐šŠ๐š•๐š•๐š๐š’๐š๐š๐šŽ๐š›๐šŽ๐š—๐š is depicted by partย (E1) of Figureย 2.3.1. It first initialises an array of counters to 0. The entries of the array correspond to the potential values of the sequence ๐šŸ๐šŠ๐š›๐šœ[0],...,๐šŸ๐šŠ๐š›๐šœ[n-1]. In a second phase the checker computes for each potential value its number of occurrences in the sequence ๐šŸ๐šŠ๐š›๐šœ[0],...,๐šŸ๐šŠ๐š›๐šœ[n-1]. This is done by scanning this sequence. Finally in a third phase the checker verifies that no value is used more than once. These three phases are represented by the automaton depicted by partย (E2) of Figureย 2.3.1. The automaton depicted by partย (E2) takes as input the sequence ๐šŸ๐šŠ๐š›๐šœ[0],...,๐šŸ๐šŠ๐š›๐šœ[n-1]. Its initial state initialises an array of counters to 0. Then it triggers successively a transition for each element ๐šŸ๐šŠ๐š›๐šœ[i] of the input sequence and increments by 1 the entry corresponding to ๐šŸ๐šŠ๐š›๐šœ[i]. The final state checks that all entries of the array of counters are strictly less than 2, which means that no value occurs more than once in the sequence ๐šŸ๐šŠ๐š›๐šœ[0],...,๐šŸ๐šŠ๐š›๐šœ[n-1].

Synthesising all the observations we got from these examples leads to the following remarks and definitions for a given global constraint ๐’ž:

  • For a given state, no transition can be triggered indicates that the constraint ๐’ž does not hold.

  • Since all transitions starting from a given state are mutually incompatible all automata are deterministic. Let โ„ณ denote the set of mutually incompatible conditions associated with the different transitions of an automaton.

  • Let ๐’ฎ 0 ,...,๐’ฎ m-1 denote the sequence of subsets of variables of ๐’ž on which the transitions are successively triggered. All these subsets contain the same number of elements and refer to some variables of ๐’ž. Since these subsets typically depend on the constraint, we leave the computation of ๐’ฎ 0 ,...,๐’ฎ m-1 outside the automaton. To each subset ๐’ฎ i of this sequence corresponds a variable S i with an initial domain ranging over [๐‘š๐‘–๐‘›,๐‘š๐‘–๐‘›+|โ„ณ|-1], where ๐‘š๐‘–๐‘› is a fixed integer. To each integer of this range corresponds one of the mutually incompatible conditions of โ„ณ. The sequences S 0 ,...,S m-1 and ๐’ฎ 0 ,...,๐’ฎ m-1 are respectively called the signature and the signature argument of the constraint. The constraint between S i and the variables of ๐’ฎ i is called the signature constraint and is denoted by ฮจ ๐’ž (S i ,๐’ฎ i ).

  • From a pragmatic point the view, the task of writing a constraint checker is naturally done by writing down an imperative program where local variables, arrays, assignment statements and control structures are used. This suggested us to consider deterministic finite automata augmented with local variables and assignment statements on these variables. Regarding control structures, we did not introduce any extra feature since the deterministic choice of which transition to trigger next seemed to be good enough.

  • Many global constraints involve a variable whose value is computed from a given collection of variables. This convinced us to allow the final state of an automaton to optionally return a result. In practice, this result corresponds to the value of a local variable of the automaton in the final state.