After class today Juan Placentia showed me a Sudoku solver he wrote. (Congratulations to Juan for taking the initiative to write it!) That made me curious about other Sudoku models. This model is a modification of a solver from the MiniZinc library. The modification involves replacing quantifications with MiniZinc's version of slices. 

The things to notice are the slices in the constraints. For example, here is the alldifferent constraint for the rows.

constraint    
    forall(i in 1..N)(alldifferent( puzzle[i,1..N] ));

alldifferent expects as its argument an array of cells. It requires them all to be different from each other. The argument to alldifferent above is a slice of the puzzle array. It refers to all the cells in row i.

The same thing is done for the alldifferent constraint for the columns. 

It's also done in a somewhat more complex way for the alldifferent constraint for the subsquares. In the subsquare constraint, the call to alldifferent looks like this.

alldifferent( puzzle[3*(i-1)+1..3*(i-1)+S, 3*(j-1)+1..3*(j-1)+S] )

The variables i and j range from 1 to 3. That means that 3*(i-1) and 3*(j-1) each take on the values: 0, 3, 6. When taken in all combinations, these are the corners of the 9 subarrays. To each of those corners, one is adding 1 .. 3 to both the row index and the column index in all combinations, thereby picking out the internal cells in that subarray.