Over the Thanksgiving break I gathered the ambition to get an extra credit assignment knocked out for my Discrete Mathematics class. We were given the opportunity to program a Sudoku solver. I chose to utilize `Python`

and the `Z3`

library that is under active development at Microsoft Research (link). The combination between Python and the Z3 library was killer! It made the solution very trivial. Let’s get right to it.

### Rules of Sudoku

If you are not familiar with the rules of Sudoku, you can read more about the rules here: Sudoku – Wikipedia. In short, there are two constraints that must be met in order to solve a Sudoku puzzle:

- Each square in the grid must contain a digit from 1 –
*n*(where*n*is the dimension of the grid). - The same digit must not appear more than once in the same column, row, or any of the sub-grids.

### Background

Z3 is a really powerful theorem prover that can be used to generate models given certain constraints. For more information and to see some examples, please see the Z3 documentation here. I was able to leverage the Z3 library to find a model given the two constraints above, and the model that Z3 generates provides at least one solution to each Sudoku puzzle (if there is a solution).

### The “*Pythonic” Way*

The code below shows how you can use Z3 to find such a model. *solve_puzzle *takes two arguments, *n* which is the dimension of the sub-grids (3 for the sample puzzle shown above), and *puzzle* which is the provided puzzle. To represent each puzzle I simply designated each empty square to be a “.”. For example, the 9×9 puzzle above would be represented as

5 3 . . 7 . . . . 6 . . 1 9 5 . . . . 9 8 . . . . 6 . 8 . . . 6 . . . 3 4 . . 8 . 3 . . 1 7 . . . 2 . . . 6 . 6 . . . . 2 8 . . . . 4 1 9 . . 5 . . . . 8 . . 7 9

For each square that is given, we add one additional constraint that the value at that square in the model must be equal to the value given in the puzzle. This is seen on line 44. After this, we have Z3 “check” if there is a model satisfying the specified constraints (line 47). If there is, then we get the model and print out the generated solution. If there is not a model that satisfies those constraints, then we know that the Sudoku puzzle is unsolvable. On lines 65-76 I added additional checks to see if the solution is unique. This is done by blocking the model of the first solution (line 69) and checking if there is an additional model that satisfies all of the previous constraints.

def solve_puzzle(n, puzzle): """ Generates a solution to the Sudoku puzzle (if one exists). :param n: The dimension of a sub-grid :param puzzle: The provided puzzle """ # For nxn sub-grids, the grid will be n^2xn^2. grid_dim = n*n; # Declare the grid for Z3 grid = [[Int("X{0}_{1}".format(i, j)) for i in range(grid_dim)] for j in range(grid_dim)] # Create a solver instance for Z3 s = Solver() # Each square in the grid must contain a digit from 1 - grid_dim for i in range(grid_dim): for j in range(grid_dim): s.add(And(1 <= grid[i][j], grid[i][j] <= grid_dim)) # Add rule for rows having distinct values for r in range(grid_dim): s.add(Distinct([grid[r]1 for c in range(grid_dim)])) # Add rule for columns being distinct for c in range(grid_dim): s.add(Distinct([grid[r]1 for r in range(grid_dim)])) # Add rule for boxes being distinct for i in range(n): for j in range(n): s.add(Distinct([grid[r]1 for c in range(i*n, i*n+n) for r in range(j*n, j*n+n)])) # Give Z3 our puzzle for i in range(grid_dim): for j in range(grid_dim): # Skip if this is a blank square if puzzle[i][j] == ".": continue # Otherwise, add a constraint that this # square == the puzzle square s.add(grid[i][j] == puzzle[i][j]) # Check if Z3 can solve the puzzle if s.check() == sat: # Get Z3's solution m = s.model() # Extract the solution into a matrix solution = [[0 for i in range(grid_dim)] for j in range(grid_dim)] for i in range(grid_dim): for j in range(grid_dim): solution[i][j] = int(str(m.eval(grid[i][j]))) # Print solution for i in range(grid_dim): row = "" for j in range(grid_dim): row = row + str(solution[i][j]) + " " print(row) # Get each declaration (d) from the current model and # create a list of constants from the declaration block = [d() != m[d] for d in m] # Add a constraint that blocks the current model, thus allowing # us to test uniqueness s.add(Or(block)) # Check if s still has a solution. If s still has a solution then the # solution is not unique if s.check() == sat: print("The solution is not unique") else: print("The solution is unique") else: print("No solution")

### Sample Usage

The sample code below shows how you can parse an input file and pass it along to the Sudoku solver. From the command line you would enter something like: `$ python sudoku.py sudoku_test1.txt`

. Each Sudoku puzzle should be entered into a text file with the first line indicating the dimension of the sub-grids and the remaining lines denoting the grid itself (as was outlined above).

if __name__ == '__main__': # grab data and parse it with open(sys.argv[1]) as f: lines = [line.strip() for line in f] # remove empty lines lines = filter(lambda x: x != "", lines) # get dim n = int(lines[0]) # split lines lines = [line.split() for line in lines[1:]] # cast ints for i in range(len(lines)): lines[i] = map(lambda x: x if x=='.' else int(x), lines[i]) # call solver solve_puzzle(n, lines)

### Conclusion

Z3 is a really powerful library! It allows you to generate complex models by describing constraints in almost plain English. We were able to program a Sudoku solver by describing the rules of Sudoku in code and then having Z3 generate a solution model for us. It can’t get easier than that.

I hope you’ve enjoyed my Sudoku nerd rage ☺. If you’d like to download my source code and test files, please feel free. I have attached them below. Thanks for reading! Happy Holidays 🎄

**Attachments:** sudoku_solver