Before splitting, the solver is stopped. As well as stopping, it is designed to output *restart nogoods* for the problem in the solver's own input language [8].

These constraints, when added to the problem, will prevent the search space just explored from being repeated in any split model2.

To split the search space for an existing model, partition the domain for the variable currently under consideration into n pieces of roughly equal size. Then create n new models and to each in turn add constraints ruling out n−1 partitions of that domain. Each one of these models restricts the possible assignments to the current variable to one nth of its domain.

As an example, consider the case n = 2. If the variable under consideration is x and its domain is {1, 2, 3, 4}, we generate 2 new models. One of them has the constraint x ≤ 2 added and the other one x ≥ 3. Thus, solving the first model will try the values 1 and 2 for x, whereas the second model will try 3 and 4.

The main problem when splitting constraint problems into parts that can be solved in parallel is that the size of the search space for each of the splits is impossible to predict reliably. This directly affects the effectiveness of the splitting however - if the search space is distributed unevenly, some of the workers will be idle while the others do most of the work.

We address this problem by providing the ability to split a constraint model after search has started. The approach is very similar to the one explained above.

The only difference is that in addition to the constraints that partition the search space, we also add constraints that rule out the search space that has been explored already.

Assume for example that we are doing 2-way branching, the variable currently under consideration is again x with domain {1, 2, 3, 4} and the branches that we have taken to get to the point where we are are x 6= 1 and x 6= 2. The generated new models will all have the constraints x 6= 1 and x 6= 2 to get to the point in the search tree where we split the problem. Then we add constraints to partition the search space based on the remaining values in the domain of x similar to the previous example.

Using this technique, we can create new chunks of work whenever a worker becomes idle by simply asking one of the busy workers to stop and generate split models. The search is then resumed from where it was stopped and the remaining search space is explored in parallel by the two workers. Note that there is a runtime overhead involved with stopping and resuming search because the constraints which enable resumption must be propagated and the solver needs to explore a small number of search nodes to get to the point where it was stopped before. There is also a memory overhead because the additional constraints need to be stored.

We have implemented this approach in a development version of Minion, which we are planning to release to the public after further testing and verifi-