## Wednesday, December 28, 2016

### 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.000ITERATION 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