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.000
ITERATION COUNT, LIMIT         0    2000000000

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

  1. KenKen puzzle solved using a MIP model:
  2. Forbid a given 0-1 solution: