3.7.208. 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.55. (A)Β The automaton for recognising the solutions to the πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint; (B)Β the automaton for recognising the non-solutions to the πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint; (C)Β the automaton for the reified πšπš•πš˜πš‹πšŠπš•_πšŒπš˜πš—πšπš’πšπšžπš’πšπš’ constraint.
ctrs/preface-195-tikz

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