cation. Initial experiments showed that the overhead of stopping, splitting and resuming is minimal and not significant for large problems.

In practice, we run Minion for a specified amount of time, then stop, split and resume instead of splitting at the beginning and when workers become idle.

The algorithm is detailed in Figure 1. This creates an n-ary split tree of models for n new models generated at each split. Initially, the potential for distribution is small but grows exponentially as more and more search is performed.

Input : constraint problem X, allotted time Tmax and splitting factor n ≥ 2 Output: a solution to X or nothing if no solution has been found run Minion with input X until termination or Tmax; if solved?(X) then terminate workers; return *solution*;
else if search space exhausted? then return; else X0 ← X with new constraints ruling out search already performed; split X0into n parts X01*, . . . , X*0n
;
for i ← 1 to n do in parallel distSolve(X0n
, Tmax,n);
end end Fig. 1. distSolve(X,Tmax,n): Recursive procedure to find the first solution to a constraint problem distributed across several workers.

## 4 Comparison To Existing Approaches

We see the main advantage of our approach in not requiring any involved changes to the constraint solving system to support distributed solving; in particular communications between workers. Conventionally, distribution is achieved with the aid of recomputation and cloning; established techniques used e.g. in [16].

We require two features of our solver: partitioning using constraints, and ability to output restart nogoods. Our system makes use of *cloning*, which we call
"splitting" and implement by means of nogoods added to the constraint model in order to partition the domain of a variable. However, where other systems use recompution, our system uses restart nogoods. In a system based on recomputation the clone begins at specific search path, e.g. stolen from another worker; with restart nogoods notionally multiple search paths are provided and the solver may explore these in any way it wishes, not necessarily one after the other. It is