If you work on a department machine, make sure you run source /course/cs195y/src/venv/bin/activate in your Terminal before working. This will place you in the course’s Python environment, which already has the Z3 library installed. Feel free to reference the Z3 Python library documentation while working on this assignment.

Problem 1: Pythagorean Triples

Three positive integers (x, y, z) such that x^2 + y^2 = z^2 form a Pythagorean triple. Euclid’s formula produces Pythageorean triples: given integers m and n such that m > n > 0, (m^2 - n^2, 2mn, m^2 + n^2) yields a Pythagorean triple.

PART 1

Using the stencil at /course/cs195y/src/smt/pythagorean.py, write a Python program to verify Euclid’s formula. Although this problem involves non-linear arithmetic, Z3 is still able to make headway and prove Euclid’s formula correct. Instead of checking within the limitation of some bounds like Alloy, Z3 checks over all mathematical integers.

PART 2

Check whether Euclid’s formula can produce non-primitive triples. A triple (x, y, z) is primitive if and only if x, y, and z share no common factors (other than 1).

Hint: For part 2, you can use the "Exists" primitive to seek a common factor.

KenKen

KenKen puzzles involve filling a n-by-n grid with digits 1 through n such that no digit appears more than once in any row or any column. Further, KenKen grids contain outlined groups of cells known as “cages” which specify both a “target” number and an arithmetic operator (addition, subtraction, multiplication, or division). The application of the specified arithmetic operator to numbers within the operator’s cage must produce the target number. KenKen addresses non-associativity of division and subtraction by restricting the cage to two squares and by not specifying an order for numbers within a cage. For example, the numbers 2 and 3 would satisfy the cage 1- as either 2,3 or 3,2.

Please read the whole problem before beginning to work.

PART 1

Using the stencil at /course/cs195y/src/smt/kenken.py, write a KenKen solver using the Z3 library in Python. To do this, add constraints to the solver inside the solve method. Following are the variables that you should use to solve the puzzle:

• self.N is the size of the board
• self.game_data is a list of cage definitions for the above puzzle.
• self.s is the solver
• self.L is a dictionary mapping indices of the board to Z3 variables. For example, self.L[(0, 1)] is the variable corresponding to the cell in row 0, column 1.

A cage definition element in self.game_data takes the following form:

dict(operation='+', number=11, cells=[(0, 0), (1, 0)])

where the field operation refers to the arithmetic operation, number refers to the target, and cells refers to the cages within the cell. We expect your constraints to accomdate KenKen puzzles of arbitrary size, so we suggest iterating over self.game_data when adding each cage constraints to your solver.

Your solve method should return any solution of the puzzle in the form of nested list, or None if it doesn’t have a solution. We provide a helper function get_grid which creates the nested list and print_grid which prints the nested list for your convenience.

PART 2

Please add another set of constraints to your solver inside check_multiple to check whether the solution found in PART 1 is the only solution to the puzzle. Your check_multiple method should return True if there is another solution to the puzzle, False otherwise.

Note: When testing, we will always run solve BEFORE check_multiple, and we will only ever run these once for each puzzle.

Feel free to use self.s.push() and self.s.pop() to manage constraints, though they are not necessary to complete the problem.

Handing In

Run cs195y_handin smt from a directory holding your 2 Python files (kenken.py and pythagorean.py). You should receive an email confirming that your handin has worked.