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

##### Figure 2.4.1. Five checkers and their corresponding automata 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],\cdots ,\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],\cdots ,\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{\to }{x}$ and $\stackrel{\to }{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]〉,\cdots ,〈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],\cdots ,\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],\cdots ,\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],$ $\cdots ,$ $\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]〉$ $,\cdots ,$ $〈\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],\cdots ,\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],\cdots ,\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],\cdots ,\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],\cdots ,\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 $𝒞$:

• 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},\cdots ,{𝒮}_{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},\cdots ,{𝒮}_{m-1}$ outside the automaton. To each subset ${𝒮}_{i}$ of this sequence corresponds a variable ${S}_{i}$ with an initial domain ranging over $\left[\mathrm{𝑚𝑖𝑛},\mathrm{𝑚𝑖𝑛}+|ℳ|-1\right]$, where $\mathrm{𝑚𝑖𝑛}$ is a fixed integer. To each integer of this range corresponds one of the mutually incompatible conditions of $ℳ$. The sequences ${S}_{0},\cdots ,{S}_{m-1}$ and ${𝒮}_{0},\cdots ,{𝒮}_{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 ${\Psi }_{𝒞}\left({S}_{i},{𝒮}_{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.