3.7.196. Reified automaton constraint

A constraint π’ž(V 1 ,V 2 ,...,V n ) for which the reified version can be mechanically constructed from the finite deterministic automaton π’œ π’ž that only accepts the set of solutions of π’ž. This is done by deriving from π’œ π’ž a so called reified automaton π’œ Β¬π’ž π’ž 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 π’œ Β¬π’ž π’ž .

  • Second, constructing from π’œ π’ž the automaton π’œ Β¬π’ž that only recognises non -solutions of π’ž.

  • Third, building from the two automata π’œ π’ž and π’œ Β¬π’ž the automaton π’œ Β¬π’ž π’ž . This is done by:

    1. Creating the initial state s of π’œ Β¬π’ž π’ž .

    2. Adding a transition labelled by value 1 from s to the initial state of π’œ π’ž .

    3. Adding a transition labelled by value 0 from s to the initial state of π’œ Β¬π’ž .

Figure 3.7.45. (A)Β The automaton for recognising the solutions of the πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint; (B)Β the automaton for recognising the non -solutions of the πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint; (C)Β the automaton for the reified πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint.
ctrs/global_contiguity_reified

FigureΒ 3.7.45 illustrates the construction of a reified automaton in the context of the πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint. PartΒ (A) recalls the automaton that only recognises the solutions of the πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint. Assuming the same alphabet {0,1}, PartΒ (B) provides the automaton that only recognises the non -solutions of the πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint. Finally, PartΒ (C) depicts the reified automaton constructed from the two automata given in partsΒ (A) andΒ (B).