Solving Sudoku with Z3

The Project

For my final project I decided I wanted to work with Z3 as I found it interesting and easy to use. Z3 is Microsoft’s satisfiability modulo theories solver (SMT), which is just a fancy way of saying that it is solver designed to determine if a solution exists for a mathematical formula. Some of you may have heard about a boolean satisfiablity solvers (SATs), which only work for boolean formulas. SMT extend SAT solvers by allowing the use of more complex functions using things like real numbers or strings. Unsure of exactly what kind of problem I wanted to tackle to using Z3, I turned to my professor Tyler who reccomended I use Z3 to solve Sudoku puzzles and as this was too simple on its own, he further requested I add an extra feature or two to my program. I thought the idea was cool, and although I hadn’t played Sudoku for more than 5 years, I remembered enough to know that it can be quite challenging and time consuming. The prospect of solving very difficult puzzles, that I myself would surely be incapable of solving in any reasonable amount of time, with just the click of a few buttons was pretty inticing.

Quick Sudoku Refresher

Sudoku is a puzzle game with a 9X9 grid that starts with a variable number of cells filled in. The goal is to then insert numbers until there is a number in every spot such that each row (ie A1-I1) and column (ie A1-A9) contain only distinct values between 1 and 9 inclusive. To make it slightly more challenging each 3X3 (ie A1-C1, A2-C2, A3-B3) box needs to contain distict values as well. Sudoku puzzles can vary wildly in difficulty with some puzzles having more square pre-filled in and potentially multiple solutions while others may have a carefully selected smaller amount of filled in elements and only a single solution. Interesting tid bit, while reading up on Sudoku I learned that any puzzle with only 7 pre-filled elements cannot have a unique solution, the minimum number required for a unique solution is still an open question is still an open question.

The Set-up

I chose to use Python, as I’ve had past experience using Z3 with Python and found it quite plesant and simple to use. The first thing I needed to do was to decide on a way to represent Sudoku. This was simple enough, intuitively I chose to represent the puzzle as a 2-D matrix with the 9 columns being the letters A-I and the 9 rows being the numbers 1-9. I’ve included an example image of what the variables for my grid looked like above. I created a simple Sudoku class with some helper functions to make things a little more simple. The class structure (print functions excluded for clarity) is shown below.

Time for Z3

Rows and Bounds

Once I had this setup, it was time to create my Z3 Solver object, and then add my Z3 variables and constraints. The most important constraint required for Sudoku was Z3’s Distict() constraint that, as its name suggests, constrains the variable list given to be distinct values. If A1 and A2 are two Z3 variables and s our solver object then s.add(Distinct(A1, A2)) constrains the solution such that A1!=A2. This is exactly what we need for Sudoku since we don’t want any values to be the same in rows, columns, or the 3x3 boxes. I added a loop that constrained each variable to either the value provided for it in the text file if supplied or to be between the bounds of 1 and 9 inclusive. To make things a little shorter at the cost of readability, I chose to add the constraints for rows in the same loop saving me from implementing another just for rows. The code for this is shown below.

Columns

The code for implementing the column constraints was implemented very similiarly to the row constraints.

Constraints for 3x3 Boxes

The hardest part of the implementation was thinking through how to iterate through the grid one 3x3 box at a time. I thought it could be done in 3 nested loops but was unable to get that working properly and settled on using 4. The code for the box constaints is shown below.

Main program

When I had my Z3 implementation worked out, it was time to work on the main program. I started by adding some code to ingest a text representation of a sudoku game. The simple text parsing code takes in the entire file, ignoring tabs and spaces, and assumes that the first 81 characters are the values for our grid where percentage symbols (%) represent the missing numbers. A sample input file is shown below. Once the text file had been ingested, I read the values into an array and printed the grid in a prettified way for the user. I could then run my constraint loops to add my constraints and variables to Z3.

Z3 Check

Once the constrains had been added correctly, finding the solution was as simple as running .check() on my solver object. If Z3 finds a model to satisfy the constraints, .check() would return z3.sat. To make it easier for the user I print this grid in a prettified way for the user. An example of the prettified inputs and outputs are shown below. **

Extra Features

Unique Solution Check

The extra feature I decided to implement was a unique solution check as suggested by Tyler. This turned out to be a lot simpler than I expected. I thought about how to imlement this check for a quite a while and experimented with a number of different ways. After getting more familiar with the object Z3.model() returns, I realized that a rather simple solution might work. First I run an initial solution check just as before and find a model that satisfies my system of constraints. I then simply add a constraint that forces at least one variable to differ from this previous model. I do this by utilizing a logical or constraint that looks like this: s.add(Or(A1 != s.model()[A1], …, I9 != s.model()[I9])). If running check() again then returns SAT then there is more than one unique solution. This idea seemed to work and although I was a bit frustrated that I spent a decent amout of time trying other ideas, I was extremely satisfied with the elegance of this solution.

Bonus extra feature

Once I had a unique solution feature, I decided that it would be easy enought to use Z3 to generate random puzzles. I acomplished this by establishing all the constraints shown above and leaving all variables in Z3 as free between the bounds. Random valid values are then added as constraints and Z3 check() used to find a valid puzzle from the seed input if possible (if not the random inputs are changed and check ran again). Once a solution is found, I have Z3 continually remove values until the unique solution check fails. When this happens the last removed value is added back and the resulting puzzle printed out.