Table 1. Shift Scheduling Problems. Ga is the acyclic grammar, Nε a is NFA with ε-transitions, Na is NFA without εtransitions, **min(**Na) is minimized NFA, A is DFA obtained from min(Na), **min(**A) is minimized A, a is the number of activities, \# is the benchmark number.

#act # Ga NF Aεa NF Aa min(NF Aa) DF A min(**DF A**)

![0_image_0.png](0_image_0.png)

straint (DFA or NFA) into CNF [10]. We compare the model that uses the PB encoding of the GRAMMAR constraint (GR1) with two models that use the PB encoding of the REGULAR constraint (REGULAR1, REGULAR2), a CP model that uses the GRAMMAR
constraint (GR
CP
1) and a CP model that uses a REGULAR constraint (REGULARCP
1).

REGULAR1 and REGULARCP
1use the DFA, whilst REGULAR2 uses the NFA constructed after simplification by when the business is closed.

The performance of a SAT solver can be sensitive to the ordering of the clauses in the formula. To test robustness of the models, we randomly shuffled each of PB instances to generate 10 equivalent problems and averaged the results over 11 instances.

Also, the GRAMMAR and REGULAR constraints were encoded into a PB formula in two different ways. The first encoding ensures that unit propagation enforces domain consistency on the constraint. The second encoding ensures that UP detects disentailment of the constraint, but does not always enforce domain consistency. For the GRAMMAR constraint we omit the same set of clauses as in [4] to obtain the weaker PB encoding. For the REGULAR constraint we omit the set of clauses that performs the backward propagation of the REGULAR constraint. Note that Table 2 shows the median time and the number of backtracks to prove optimality over 11 instances. For each model we show the best median time and the corresponding number of backtracks for the PB encoding that achieves domain consistency and for the weaker encoding.

Table 2 shows the results of our experiments using these 5 models. The model REGULAR2 outperforms GR1 in all benchmarks, whilst model REGULAR1 outperforms GR1 in most of the benchmarks. The model REGULAR2 also proves optimality in several instances of hard benchmarks. It should be noted that performing simplification before minimization is essential. It significantly reduces the size of the encoding and speeds up MiniSat+ by factor of 54. Finally, we note that the PB models consistently outperformed the CP models, in agreement with the observations of [4]. Between the two CP models, REGULARCP
1is significantly better than GR
CP
1, finding a better solution in many instances and proving optimality in two instances. In addition, although we do not show it in the table, Gecode is approximately three orders of magnitude faster per branch with the REGULARCP
1 model. For instance, in benchmark number 2 with 1 activity and 4 workers, it explores approximately 80 million branches with the REGULARCP
1and 24000 branches with the GR
CP
1 model within the 1 hour timeout.

4 Due to lack of space we do not show these results