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...