Inspired by the SAT-based Sudoku solver by Tjark Weber and the corresponding Python implementation, I coded up a quick SAT-based KenKen solver.

The ideas in the KenKen solver are pretty similar to the Sudoku solver. In particular, we reuse the framework of using a boolean variable to represent
each possible digit in each cell and all of the clauses which correspond to the following rules:

• At least one digit must be present in a cell
• Two or more digits may not be present in a cell
• The same digit may not appear more than once in any row
• The same digit may not appear more than once in any column

To satisfy the mathematical expressions, we generate all list of all possible ways each “cage” can be filled. This is most naturally expressed in disjunctive normal form:

(cell1 has value v1 AND cell2 has value v2 AND ...)
OR (cell1 is value w1 AND cell2 has value w2 AND ...)
OR ...

This can be easily and efficiently transformed into a equisatisfiable conjunctive normal form by adding a few auxiliary variables.

The SAT-based solver is reasonably fast. For example, on my laptop it can solve a 6-by-6 KenKen problem in about 23 ms. On a big a 9-by-9 problem it takes about 328 ms which is a factor of 5 or so slower than the NekNek solver (which takes about 65 ms).