A first systematic approach for creating an automaton that only recognises the solutions to the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}$ constraint could be to:

• First, create an automaton that recognises the solutions to the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}$ constraint.

• Second, create an automaton that recognises the solutions to the $\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}\_\mathrm{𝚕𝚘𝚠}\_\mathrm{𝚞𝚙}$ constraint.

• Third, make the product of the two previous automata and minimise the resulting automaton.

However this approach is not going to scale well in practice since the automaton associated with the $\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}\_\mathrm{𝚕𝚘𝚠}\_\mathrm{𝚞𝚙}$ constraint may have a too big size. Therefore we propose an approach where we directly construct in a single step the automaton that only recognises the solutions to the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}$ constraint. Note that we do not have any formal proof that the resulting automaton is always minimum.

Without loss of generality, we assume that:

• All items of the $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}$ collection are sorted in increasing value on the attribute $\mathrm{𝚟𝚊𝚕}$.

• All the potential values of the variables of the $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$ collection are included within the set of values of the collection $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}$ (i.e., the $\mathrm{𝚟𝚊𝚕}$ attribute).If this is not the case, we can include these values within the $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}$ collection and set their minimum and maximum number of occurrences to 0 and $\left|\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right|-{\sum }_{v=1}^{\left|\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\right|}\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚒𝚗}$.

• All values of the $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}$ collection for which the attribute $\mathrm{𝚘𝚖𝚊𝚡}$ is set to 0 cannot be assigned to the variables of the $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$ collection.We initially remove such values from all variables of the $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$ collection.

Before defining the states of the automaton, we first need to introduce the following notion. A value $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ is constrained by its maximum number of occurrences if and only if $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚊𝚡}\le 1\vee \mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚊𝚡}<\left|\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right|-{\sum }_{u=1,u\ne v}^{\left|\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\right|}\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[u\right].\mathrm{𝚘𝚖𝚒𝚗}$.When $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚊𝚡}\le 1$ we cannot reduce the number of states related to value $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ and we therefore consider that we are in the constrained case. Let $𝒱$ denote the set of constrained values (i.e., their indexes within the collection $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}$) by their respective maximum number of occurrences.

After determining the set $𝒱$, the $\mathrm{𝚘𝚖𝚊𝚡}$ attribute of each potential value is normalised in the following way:

• For an unconstrained value $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ we reset $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚊𝚡}$ to $max(1,\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}[v].\mathrm{𝚘𝚖𝚒𝚗})$.

• For a constrained value $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ we reset $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚊𝚡}$ to 1 if its current value is smaller than 1.

We are now in position to introduce the states of the automaton.

The $1+{\sum }_{v=1,v\in 𝒱}^{\left|\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\right|}\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚊𝚡}+{\sum }_{v=1,v\notin 𝒱}^{\left|\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\right|}\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚒𝚗}$ states of the automaton that only accepts solutions to the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}$ constraint are defined in the following way:

• For the $v^{\mathrm{𝑡ℎ}}$ item of the collection $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}$ we have:

  • If $v\in 𝒱$, $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚊𝚡}$ states labelled by $s_{vo}$ $(1\le o\le \mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}[v].\mathrm{𝚘𝚖𝚊𝚡})$.

  • If $v\notin 𝒱$, $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚒𝚗}$ states labelled by $s_{vo}$ $(1\le o\le \mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}[v].\mathrm{𝚘𝚖𝚒𝚗})$.

• We have an initial state labelled by $s_{00}$.

Terminal states correspond to those states $s_{vo}$ such that, both (1) $o$ is greater than or equal to $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚒𝚗}$, and (2) there is no value item $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[w\right]$ $(w>v)$ such that $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[w\right].\mathrm{𝚘𝚖𝚒𝚗}>0$. Transitions are defined in the following way:

• There is an arc, labelled by $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$, from the initial state $s_{00}$ to every state $s_{v1}$ where $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right]$ is an item for which all values $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[u\right].\mathrm{𝚟𝚊𝚕}$ strictly less than $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ verify the condition $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[u\right].\mathrm{𝚘𝚖𝚒𝚗}=0$.

• For each value $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ constrained by its maximum number of occurrences (i.e., $v\in 𝒱$), there is an arc, labelled by $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$, from the state $s_{vk}$ to the state $s_{vk+1}$ for all $k$ in $[1,\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}[v].\mathrm{𝚘𝚖𝚊𝚡}-1]$.

• For each value $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ unconstrained by its maximum number of occurrences (i.e., $v\notin 𝒱$), there is an arc, labelled by $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$, from the state $s_{vk}$ to the state $s_{vk+1}$ for all $k$ in $[1,\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}[v].\mathrm{𝚘𝚖𝚒𝚗}-1]$. There is also a loop, labelled by $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$, from state $s_{vk}$ to the state $s_{vk}$ for $k=\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚒𝚗}$.

• For each value $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ constrained by its maximum number of occurrences (i.e., $v\in 𝒱$), there is an arc, labelled by $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[w\right].\mathrm{𝚟𝚊𝚕}$, from state $s_{vk}$ to state $s_{w1}$ $(v<w)$ for all $k$ in $\left[\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\right[v].\mathrm{𝚘𝚖𝚒𝚗},\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}[v].\mathrm{𝚘𝚖𝚊𝚡}]$ and for all $w$ such that $\forall u\in [v+1,w-1]:\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[u\right].\mathrm{𝚘𝚖𝚒𝚗}=0$.

• For each value $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚟𝚊𝚕}$ unconstrained by its maximum number of occurrences (i.e., $v\notin 𝒱$), there is an arc, labelled by $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[w\right].\mathrm{𝚟𝚊𝚕}$, from state $s_{vk}$ to state $s_{w1}$ $(v<w)$ for $k=\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[v\right].\mathrm{𝚘𝚖𝚒𝚗}$ and for all $w$ such that $\forall u\in [v+1,w-1]:\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}\left[u\right].\mathrm{𝚘𝚖𝚒𝚗}=0$.

Figure 5.186.2 depicts the automaton associated with the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}$ constraint of the Example slot. For this purpose we assume without loss of generality that we have four decision variables that all take their potential values within interval $[3,8]$. Consequently, values 4, 7 and 8 are first added to the items of the $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}$ collection. Both values 3 and 6 are unconstrained by their respective maximum number of occurrences. Therefore their $\mathrm{𝚘𝚖𝚊𝚡}$ attributes are respectively reduced to 2 and 1. All other values, namely values 4, 5, 7 and 8, are constrained values. The $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}$ constraint holds since the corresponding sequence of visited states, $s_{00}$ $s_{11}$ $s_{12}$ $s_{41}$ $s_{61}$, ends up in an accepting state (i.e., accepting states are denoted graphically by a double circle in the figure). Note that non initial states are first indexed by the position of an item within the $\mathrm{𝚅𝙰𝙻𝚄𝙴𝚂}$ collection, and not by the value itself (e.g., within $s_{12}$ the 1 designates value 3). For instance state $s_{11}$ depicts the fact that the automaton has already recognised a single occurrence of value 3, while $s_{12}$ corresponds to the fact that the automaton has already seen at least two occurrences of value 3.The at least comes from the loop on state $s_{12}$.

Figure 5.186.2. Automaton of the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}$ constraint of the Example slot: the path corresponding to the solution $\langle \mathbf{3},\mathbf{3},\mathbf{6},\mathbf{8}\rangle$ is depicted by thick orange arcs