### 2.4.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:

Partsย (A1), (B1), (C1), (D1) andย (E1) of Figureย 2.4.1 depict the five checkers respectively associated with $\mathrm{๐๐๐๐๐๐}_\mathrm{๐๐๐๐๐๐๐๐๐๐ข}$, with $\mathrm{๐๐๐ก}_\mathrm{๐๐๐๐๐๐}$, with $\mathrm{๐๐๐๐๐}$, with $\mathrm{๐๐๐๐๐๐ก๐๐๐}$ and with $\mathrm{๐๐๐๐๐๐๐๐๐๐๐๐}$. Within the corresponding automata an initial state is indicated by an arc coming from no state and an accepting state is denoted graphically by a double circle. For each checker we observe the following facts:

• Within the checker depicted by partย (A1) of Figureย 2.4.1, the values of the sequence $\mathrm{๐๐๐๐}\left[0\right],โฏ,\mathrm{๐๐๐๐}\left[n-1\right]$ 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.4.1. The automaton takes as input the sequence $\mathrm{๐๐๐๐}\left[0\right],โฏ,\mathrm{๐๐๐๐}\left[n-1\right]$, and triggers successively a transition for each term of this sequence. Transitions labelled by 0 and 1 are respectively associated with the conditions $\mathrm{๐๐๐๐}\left[i\right]=0$ and $\mathrm{๐๐๐๐}\left[i\right]=1$.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.4.1, the components of vectors $\stackrel{โ}{x}$ and $\stackrel{โ}{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.4.1. The automaton takes as input the sequence $โฉx\left[0\right],y\left[0\right]โช,โฏ,โฉx\left[n-1\right],y\left[n-1\right]โช$ and triggers a transition for each term of this sequence. Unlike the $\mathrm{๐๐๐๐๐๐}_\mathrm{๐๐๐๐๐๐๐๐๐๐ข}$ constraint, some transitions now correspond to a condition (e.g.,ย $x\left[i\right]=y\left[i\right]$, $x\left[i\right]) between two variables of the $\mathrm{๐๐๐ก}_\mathrm{๐๐๐๐๐๐}$ constraint.

• Note that the $\mathrm{๐๐๐๐๐}$$\left(\mathrm{๐๐๐๐},$ $\mathrm{๐๐๐๐},$ $\mathrm{๐๐๐๐๐๐}\right)$ constraint involves a variable $\mathrm{๐๐๐๐}$ whose value is computed from a given collection of variables $\mathrm{๐๐๐๐}$. The checker depicted by partย (C1) of Figureย 2.4.1 counts the number of variables of $\mathrm{๐๐๐๐}\left[0\right],โฏ,\mathrm{๐๐๐๐}\left[n-1\right]$ that take their values in $\mathrm{๐๐๐๐๐๐}$. For this purpose it uses a counter $c$, which is possibly tested against the value of $\mathrm{๐๐๐๐}$. 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 accepting states of an automaton can force a variable of the constraint to be equal to a given counter. Partย (C2) of Figureย 2.4.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 $\mathrm{๐๐๐๐}\left[0\right],โฏ,\mathrm{๐๐๐๐}\left[n-1\right]$. It triggers a transition for each variable of this sequence and increments $c$ when the corresponding variable takes its value in $\mathrm{๐๐๐๐๐๐}$. The accepting state returns a success when the value of $c$ is equal to $\mathrm{๐๐๐๐}$. 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 $\mathrm{๐๐๐๐}$. In addition, it would require more states than the automaton of partย (C2) of Figureย 2.4.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 $\mathrm{๐๐๐๐๐}$ constraint, the $\mathrm{๐๐๐๐๐๐ก๐๐๐}$$\left(\mathrm{๐๐๐๐},\mathrm{๐๐๐๐}\right)$ constraint involves a variable $\mathrm{๐๐๐๐}$ whose value is computed from a given sequence of variables $\mathrm{๐๐๐๐}\left[0\right],$ $โฏ,$ $\mathrm{๐๐๐๐}\left[n-1\right]$. Therefore, the checker depicted in partย (D1) of Figureย 2.4.1 uses also a counter $c$ for counting the number of inflexions, and compares its final value to the $\mathrm{๐๐๐๐}$ argument. The automaton depicted by partย (D2) of Figureย 2.4.1 represents this program. It takes as input the sequence of pairs $โฉ\mathrm{๐๐๐๐}\left[0\right],\mathrm{๐๐๐๐}\left[1\right]โช,$ $โฉ\mathrm{๐๐๐๐}\left[1\right],\mathrm{๐๐๐๐}\left[2\right]โช$ $,โฏ,$ $โฉ\mathrm{๐๐๐๐}\left[n-2\right],\mathrm{๐๐๐๐}\left[n-1\right]โช$ 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 $\mathrm{๐๐๐๐}\left[0..n-1\right]$ and increments the counter $c$ when a new inflexion is detected. The accepting state returns a success when the value of $c$ is equal to $\mathrm{๐๐๐๐}$.

• The checker associated with $\mathrm{๐๐๐๐๐๐๐๐๐๐๐๐}$ is depicted by partย (E1) of Figureย 2.4.1. It first initialises an array of counters to 0. The entries of the array correspond to the potential values of the sequence $\mathrm{๐๐๐๐}\left[0\right],โฏ,\mathrm{๐๐๐๐}\left[n-1\right]$. In a second phase the checker computes for each potential value its number of occurrences in the sequence $\mathrm{๐๐๐๐}\left[0\right],โฏ,\mathrm{๐๐๐๐}\left[n-1\right]$. 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.4.1. The automaton depicted by partย (E2) takes as input the sequence $\mathrm{๐๐๐๐}\left[0\right],โฏ,\mathrm{๐๐๐๐}\left[n-1\right]$. Its initial state initialises an array of counters to 0. Then it triggers successively a transition for each element $\mathrm{๐๐๐๐}\left[i\right]$ of the input sequence and increments by 1 the entry corresponding to $\mathrm{๐๐๐๐}\left[i\right]$. The accepting 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 $\mathrm{๐๐๐๐}\left[0\right],โฏ,\mathrm{๐๐๐๐}\left[n-1\right]$.

Synthesising all the observations we got from these examples leads to the following remarks and definitions for a given global constraint $\mathrm{๐}$:

• For a given state, no transition can be triggered indicates that the constraint $\mathrm{๐}$ does not hold.

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

• Let ${\mathrm{๐ฎ}}_{0},โฏ,{\mathrm{๐ฎ}}_{m-1}$ denote the sequence of subsets of variables of $\mathrm{๐}$ on which the transitions are successively triggered. All these subsets contain the same number of elements and refer to some variables of $\mathrm{๐}$. Since these subsets typically depend on the constraint, we leave the computation of ${\mathrm{๐ฎ}}_{0},โฏ,{\mathrm{๐ฎ}}_{m-1}$ outside the automaton. To each subset ${\mathrm{๐ฎ}}_{i}$ of this sequence corresponds a variable ${S}_{i}$ with an initial domain ranging over $\left[\mathrm{๐๐๐},\mathrm{๐๐๐}+|\mathrm{โณ}|-1\right]$, where $\mathrm{๐๐๐}$ is a fixed integer. To each integer of this range corresponds one of the mutually incompatible conditions of $\mathrm{โณ}$. The sequences ${S}_{0},โฏ,{S}_{m-1}$ and ${\mathrm{๐ฎ}}_{0},โฏ,{\mathrm{๐ฎ}}_{m-1}$ are respectively called the signature and the signature argument of the constraint. The constraint between ${S}_{i}$ and the variables of ${\mathrm{๐ฎ}}_{i}$ is called the signature constraint and is denoted by ${\mathrm{ฮจ}}_{\mathrm{๐}}\left({S}_{i},{\mathrm{๐ฎ}}_{i}\right)$.

• 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 accepting 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 accepting state.