Proof: To show | min(unfold n(A))| ≤ |unfold n**(min(**A))|, we observe that both min(**unfold** n(A)) and unfold n**(min(**A)) are automata that recognize the same language. By definition, minimization returns the smallest DFA accepting this language.

Hence min(**unfold** n(A)) cannot be larger than unfold n**(min(**A)).

To show unfolding then minimizing can give an exponentially smaller sized DFA,
consider the following language L. A string of length k belongs to L iff it contains the symbol j, j = k mod n, where n is a given constant. The alphabet of the language L is {0**, . . . , n** − 1}. The minimal DFA for this language has Ω(n2 n) states as each state needs to record which symbols from 0 to n − 1 have been seen so far, as well as the current length of the string mod n. Unfolding this minimal DFA and restricting it to strings of length n gives an acyclic DFA with Ω(n2 n) states. Note that all strings are of length n and the equation j = n mod n has the single solution j = 0. Therefore, the language L consists of the strings of length n that contain the symbol 0. On the other hand, if we unfold and then minimize, we get an acyclic DFA with just 2n states. Each layer of the DFA has two states which record whether 0 has been seen. ⊓⊔
Further, if we make our initial problem domain consistent, domains might be pruned which give rise to possible simplifications of the DFA. We show here that we should also perform such simplification before minimizing.

Theorem 4. *Given any DFA* A, | min(simplify(unfoldn(A)))| ≪
|simplify(min(**unfold** n
(A)))|.

Proof: Both min(simplify(**unfold**n
(A))) and simplify(min(**unfold** n
(A))) are DFAs that recognize the same language of strings of length n. By definition, minimization must return the smallest DFA accepting this language. Hence min(simplify(unfoldn(A))) is no larger than simplify(min(unfold n(A))).

To show that minimization after simplification may give an exponentially smaller sized automaton, consider the language which contains sequences of integers from 1 to n in which at least one integer is repeated and in which the last two integers are different. The alphabet of the language L is {1**, . . . , n**}. The minimal unfolded DFA for strings of length n from this language has Ω(2n) states as each state needs to record which integers have been seen.Suppose the integer n is removed from the domain of each variable. The simplified DFA still has Ω(2n) states to record which integers 1 to n − 1 have been seen.On the other hand, suppose we simplify before we minimize. By a pigeonhole argument, we can ignore the constraint that an integer is repeated. Hence we just need to ensure that the string is of length n and that the last two integers are different. The minimal DFA accepting this language requires just O(n) states. ⊓⊔

## 6 Empirical Results

We empirically evaluated the results of our method on a set of shift-scheduling benchmarks [11, 14] 3. Experiments were run with the Minisat+ solver for pseudo-Boolean 3 We would like to thank Louis-Martin Rousseau and Claude-Guy Quimper for providing us with the benchmark data