3.7.208. Reified automaton constraint
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
.
A constraint
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 in front of the sequence of variables .
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:
Creating the initial state of .
Adding a transition labelled by value 1 from to the initial state of .
Adding a transition labelled by value 0 from to the initial state of .
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 , 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).