Unique Solutions in KenKen

In (1) a MIP model is proposed so solve the KenKen puzzle. During a discussion, the question came up if I could prove the uniqueness of a solution. In the Mixed Integer Programming model I used a standard formulation for a solution: 

$$x_{i,j,k} = \begin{cases}1 & \text{if cell $(i,j)$ has the value $k$}\\                                     0 & \text{otherwise}\end{cases}$$

A general approach could be to use the technique described in (2): add a cut to forbid the current solution and solve again. If this second solve is infeasible we have established that the original solution was unique.

In this case we can use a more specialized cut that is simpler:

$$\sum_{i,j,k} x^*_{i,j,k} x_{i,j,k} \le n^2-1$$

where $x^*$ is the previous solution and $n \times n$ is the size of the puzzle.

To test this with the model and problem data shown in (1) I used:

Note that $\displaystyle\sum_{i,j,k|x^*_{i,j,k}=1} x_{i,j,k}$ is identical to $\displaystyle\sum_{i,j,k} x^*_{i,j,k} x_{i,j,k}$. To make sure things work correctly with solution values like 0.9999, I actually used a somewhat generous tolerance: $\displaystyle\sum_{i,j,k|x^*_{i,j,k}>0.5} x_{i,j,k}$.

Indeed the solution from the first solve was unique. The second solve yielded:

S O L V E      S U M M A R Y      MODEL   kenken2             OBJECTIVE  z      TYPE    MIP                 DIRECTION  MINIMIZE      SOLVER  CPLEX               FROM LINE  115 **** SOLVER STATUS     1 Normal Completion         **** MODEL STATUS      10 Integer Infeasible       **** OBJECTIVE VALUE               NA RESOURCE USAGE, LIMIT          0.031      1000.000 ITERATION COUNT, LIMIT         0    2000000000

This approach can also be applied to the Sudoku MIP model.

References

1. KenKen puzzle solved using a MIP model: http://yetanothermathprogrammingconsultant.blogspot.com/2016/10/mip-modeling-from-sudoku-to-kenken.html
2. Forbid a given 0-1 solution: http://yetanothermathprogrammingconsultant.blogspot.com/2011/10/integer-cuts.html