AND-NODE to p
′. This vertex is in Gv by line 7. By the construction of Γ(p) in the proof of theorem 1, a symbol is placed on the stack if and only if it is the right child of an AND-NODE, hence if and only if it appears in p
′. Moreover, if a vertex is the i th vertex in a path, it corresponds to the i th element from the top of Γ(p). We now see that p
′is unique for Γ(p). Two distinct paths of length k cannot map to the same stack configuration, because they must differ in at least one position i, therefore they correspond to stacks with different symbols at position i. Therefore, there exists a bijection between paths in Gv and stack configurations with v at the top. ⊓⊔
Hence |Q(Ng)| =Pv \#**paths**(Gv), where v is an OR-NODE of Ga. Computing the stack graph Gv of every OR-NODE v takes O(|Ga|) time, as does counting paths in Gv. Therefore, computing the number of states in Na takes O(|Ga| 2) time. We can also compute the number of states in the ε-closure of Na by observing that if none of the OR-NODES that are reachable by paths of length 2 from an OR-NODE v correspond to terminals, then any state that corresponds to a stack configuration with v at the top will only have outgoing ε−transitions and will be removed by the ε−closure. Thus, to compute the number of states in Na after ε−closure, we sum the number of paths in Gv for all OR-NODES v such that a terminal OR-NODE can be reached from v by a path of length 2.

## 4.5 Transformation Into A Dfa

Finally, we convert the NFA into a DFA using the standard subset construction. This is optional as Pesant's propagator for the REGULAR constraints works just as well with NFAs as DFAs. Indeed, removing non-determinism may increase the size of the automaton and slow down propagation. However, converting into a DFA opens up the possibility of further optimizations. In particular, as we describe in the next section, there are efficient methods to minimize the size of a DFA. By comparison, minimization of a NFA is PSPACE-hard in general [7]. Even when we consider just the acyclic NFA constructed by unfolding a NFA, minimization remains NP-hard [8].

## 5 Automaton Minimization

The DFA constructed by this or other methods may contain redundant states and transitions. We can speed up propagation of the REGULAR constraint by minimizing the size of this automaton. Minimization can be either offline (i.e. before we have the problem data and have unfolded the automaton) or online (i.e. once we have the problem data and have unfolded the automaton). There are several reasons why we might prefer an online approach where we unfold before minimizing. First, although minimizing after unfolding may be more expensive than minimizing before unfolding, both are cheap to perform. Minimizing a DFA takes O(Q log Q) time using Hopcroft's algorithm and O(nQ) time for the unfolded DFA where Q is the number of states [9]. Second, thanks to Myhill-Nerode's theorem, minimization does not change the layered nature of the unfolded DFA. Third, and perhaps most importantly, minimizing a DFA after unfolding can give an exponentially smaller automaton than minimizing the DFA and then unfolding. To put it another way, unfolding may destroy the minimality of the DFA.