Assignment 2: Encoding the KenKen puzzle into SMT

The KenKen Puzzle

KenKen is a popular logic/arithmetic puzzle that was invented in 2004. It is similar to Sudoku since the goal is to fill in a grid with digits, where no digits can appear twice in the same row or column. However, in solving a KenKen puzzle arithmetic reasoning is involved, since digits are filled in such that they produce certain target numbers using prescribed arithmetic operations. Please read the Wikipedia KenKen page Links to an external site. for a detailed description of the KenKen puzzle.

Your Task

Your task is to write a program that converts a KenKen problem into a Z3 (i.e., SMT) formula such that a satisfying assignment for the generated formula (when appropriately translated) gives you a solution for the KenKen problem (if one exists). Your implementation should have a reasonable runtime, meaning that a 6x6 puzzle should be solved in under one minute. Thoroughly test your implementation (you can find puzzle generators online).

We provide a simple reference implementation skeleton in Python that parses our prescribed input format for you: kenken.py
Download kenken.py

In addition, we provide several input files as examples: kenken_test1.txt Download kenken_test1.txt

You can fine their respective solutions (the format should be self-explanatory) here: kenken_solution1.txt Download kenken_solution1.txt

Referring to our reference implementation, the puzzle list contains lists representing the cages in the puzzle. More specifically, puzzle[i][0] holds the goal for the operation, puzzle[i][1] contains the operation to be used for the cage. The operations will be ’+’, ’-’, ’*’, ’/’ and ’g’ which denote addition, subtraction, multiplication, division, and "given", respectively. Here ”given” means that the goal is the value of the indicated square. For cages using division or subtraction, you may assume that the cage has two squares in it. Since these operations are not commutative you will have to assert for squares a and b that a/b == goal or b/a == goal is true. Finally, for a cage list cage, cage[2*i] holds the row of the grid and cage[2*i+1] holds the column of the grid where i is in the interval [1, len(cage)). These two values indicate the coordinate of a square in the grid.

An example of a cage is:
cage = [11, ’+’, 0, 0, 1, 0, 1, 1]
This means that the goal is 11, the operation is addition and the cage is on the squares (0,0), (1,0) and (1,1).

Here are some additional notes:

• I recommend you use only the theory of integer arithmetic.
• I recommend that you use Z3 Links to an external site. as your SMT solver, but there are many other SMT solvers that you can take a look at (see SMT-COMP Links to an external site.). You can either invoke it as an external command from your program or use it as a library. Z3 also has a really handy Python interface that can make your job easier (no need to write to files and parse Z3 output). To learn more about Z3Py check out this tutorial Links to an external site.. You can assume that Z3 is in the PATH variable on our grading machine. If you prefer to use a different SMT solver, submit its binary with your solution.
• This is a graduate/advanced undergraduate level class, and I am expecting of students at this level to be able to deal with unspecified or under-specified details of an assignment. Discovering such potential issues on your own and dealing with them is a part of the learning process. Hence, please do not hesitate to ask clarification questions through Canvas.
• Do let us know ASAP if you get stuck installing Z3 and/or Z3py on your machine!

Assignment Deliverables

Source code and a Linux binary of your solution if applicable. Also, a brief summary (at most one page, PDF format) explaining how your encoding works and how to run your solution. Ultimately, we have to be able to run your solution on a Linux machine. Submit your deliverables (PDF summary, source code, binary if applicable) as an archive (zip, tgz) through Canvas.