Sudoku Generator

 Overview

Developed the game "Sudoku" using Python and the Z3 API. Z3 is a theorem solver that we utilized to randomly generate Sudoku puzzles. This required us to create solver constraints that correspond to Sudoku rules. Our solver serves the purpose of generating 81 numbers that correspond to the 9x9 board of Sudoku. These numbers are constrained in that they must be between 1 and 9, inclusive. The rows of the board must not contain any of the same number. The same is true of the columns and each 3x3 subsection of the board.

Figure 1: Image of one randomly generated Sudoku Board in the Visual Studio Code terminal

In-Depth Explanation of Project and Methods

      The scope of the project was to create a sudoku game in python that can be played within the terminal. To accomplish this we also needed to create a sudoku solver so that we could check the board we were generating to make sure it was solvable and that it only had one solution, or in other words that it had a unique solution. The Solver was also necessary to check whether or not an entered number was correct or not. The motivation behind creating this sudoku game was that we wanted to create an interactive project that a user could have fun with, and the best option to accommodate these conditions was sudoku. In addition to wanting to make a fun interactive project we also played sudoku before this project and wanted to create our own sudoku games that we can play. Our goals in this project was to create a fully functioning sudoku game that creates unique games every time and will be able to tell if a given input is correct or if it will make the rest of the game unsolvable and that it will notify the user if they pick an incorrect value for a given row and column. We were able to achieve all of these goals as we did create a fully functional sudoku game that is able to check a user's work and is capable of generating a unique sudoku board everytime the program is run.       

     For the actual coding of our Sudoku project, we decided that we should create several functions that would handle generation of the Sudoku puzzle and several functions that would handle the user interface / gameplay portion of our project. For the generation of the puzzle, we also decided that the best method would be to use a z3 sat solver to create a filled in board. This filled in board was generated by creating a solver with constraints that tell the solver that there should be 81 numbers, the numbers in rows / columns / subsections should be distinct, and the values of the numbers should be between 1 and 9 inclusive. With these constraints, we passed the solver to a function called generateSudoku(s) that converts the values of the solver model into a 9x9 array of integers, and returns that array. We randomized the generation of the board by blocking the solution of the solver a random amount of times so that the board generated would not be the same every time the code is run. 

     After generating the puzzle as a 9x9 array, we developed a method to take out numbers from the puzzle so that the board would not be fully filled out. We started this by using a function called reduceSudoku(Board). This function randomly selects a position in the 9x9 array and replaces the number in that position with zero. We then added a constraint to the solver saying that the solution must contain the numbers that are in the board returned by reduceSudoku(Board). We put this process into a while loop so that it would continuously take out numbers from the puzzle until the solution to the puzzle was not unique. We then saved the most recent puzzle that generated a unique solution by saving the previous generated puzzle to a variable called PrevBoard, which concluded the generation of the initial board.      The last step was then to create the gameplay portion of the project. This step was fairly simple, as all we had to do was print the 9x9 array that is the puzzle and then take and check input from the user. This step was completed by using the input function in python to ask the user for a row, column, and value. We then implemented checks to make sure that the inputs were in the range of 1 to 9, and issued error messages if they were not. We also made checks to issue error messages if the user placed a number that would not lead to the solution, or if they tried to input a number in a spot that was already filled. This portion of the code was placed inside of a while loop to continuously print the puzzle and ask for input until the board was solved. Once the board is solved, the program prints a message notifying the user, and then the program terminates. In order for the user to play another game they must call python Sudoku.py again from the terminal.      

     This project over all was a complete success because we were able to create a fully functional sudoku game that is capable of generating unique sudoku boards and being able to solve the game so as to notify the user if their input was correct. While our project works and accomplishes all that we wanted it too there are still a couple of problems and features that we did not get to but we would have liked to add if we had more time. The main problem that we would want to look into is if there is any way to create a unique board in a shorter amount of time. Our current project creates a sudoku board in 45 seconds to a minute, and while this is not an outrageous amount of time, we would want to shorten that time if we were given more time. We are not sure of the best way to decrease the time for creating a unique board, but some things we might try would be to create the sudoku board without using the z3 solver and instead creating it by ourselves. This solution to the time problem would mean that after several random numbers were generated on the board​,​ we would have to be less random and more methodical about filling in the rest of the board so that the full board will be able to be created in a timely manner.​ ​The features that we wanted to include multiple levels of difficulty that would be user selectable, but we did not have enough time to complete this feature for our project. The way we most likely would have created these different levels, would be to limit the number of numbers we take out after we have a complete sudoku board. This would make it so that the easier levels would remove less numbers and the hardest level would remove as many as it could before it created a non-unique solution. 

Download the code here: https://github.com/MauriceTakeda/Python-Z3-Sudoku-Generator