### 3.7.196. Reified automaton constraint

A constraint $\mathrm{\pi }\left({V}_{1},{V}_{2},...,{V}_{n}\right)$ for which the reified version can be mechanically constructed from the finite deterministic automaton ${\mathrm{\pi }}^{\mathrm{\pi }}$ that only accepts the set of solutions of $\mathrm{\pi }$. This is done by deriving from ${\mathrm{\pi }}^{\mathrm{\pi }}$ a so called reified automaton ${\mathrm{\pi }}_{Β¬\mathrm{\pi }}^{\mathrm{\pi }}$ by:

• First, adding a 0-1 variable $B$ in front of the sequence of variables ${V}_{1},{V}_{2},...,{V}_{n}$. This new sequence of variables will be passed to the reified automaton ${\mathrm{\pi }}_{Β¬\mathrm{\pi }}^{\mathrm{\pi }}$.

• Second, constructing from ${\mathrm{\pi }}^{\mathrm{\pi }}$ the automaton ${\mathrm{\pi }}_{Β¬\mathrm{\pi }}$ that only recognises non -solutions of $\mathrm{\pi }$.

• Third, building from the two automata ${\mathrm{\pi }}^{\mathrm{\pi }}$ and ${\mathrm{\pi }}_{Β¬\mathrm{\pi }}$ the automaton ${\mathrm{\pi }}_{Β¬\mathrm{\pi }}^{\mathrm{\pi }}$. This is done by:

1. Creating the initial state $s$ of ${\mathrm{\pi }}_{Β¬\mathrm{\pi }}^{\mathrm{\pi }}$.

2. Adding a transition labelled by value 1 from $s$ to the initial state of ${\mathrm{\pi }}^{\mathrm{\pi }}$.

3. Adding a transition labelled by value 0 from $s$ to the initial state of ${\mathrm{\pi }}_{Β¬\mathrm{\pi }}$.

FigureΒ 3.7.45 illustrates the construction of a reified automaton in the context of the $\mathrm{\pi \pi \pi \pi \pi \pi }_\mathrm{\pi \pi \pi \pi \pi \pi \pi \pi \pi \pi ’}$ constraint. PartΒ (A) recalls the automaton that only recognises the solutions of the $\mathrm{\pi \pi \pi \pi \pi \pi }_\mathrm{\pi \pi \pi \pi \pi \pi \pi \pi \pi \pi ’}$ constraint. Assuming the same alphabet $\left\{0,1\right\}$, PartΒ (B) provides the automaton that only recognises the non -solutions of the $\mathrm{\pi \pi \pi \pi \pi \pi }_\mathrm{\pi \pi \pi \pi \pi \pi \pi \pi \pi \pi ’}$ constraint. Finally, PartΒ (C) depicts the reified automaton constructed from the two automata given in partsΒ (A) andΒ (B).