From be3edb60f91aa1036f2ed0b00d2ad0665e6d6343 Mon Sep 17 00:00:00 2001 From: udlbook <110402648+udlbook@users.noreply.github.com> Date: Sat, 19 Apr 2025 16:35:23 -0400 Subject: [PATCH] Created using Colab --- Trees/SAT_Sudoku.ipynb | 272 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 272 insertions(+) create mode 100644 Trees/SAT_Sudoku.ipynb diff --git a/Trees/SAT_Sudoku.ipynb b/Trees/SAT_Sudoku.ipynb new file mode 100644 index 0000000..32b6a4a --- /dev/null +++ b/Trees/SAT_Sudoku.ipynb @@ -0,0 +1,272 @@ +{ + "nbformat": 4, + "nbformat_minor": 0, + "metadata": { + "colab": { + "provenance": [], + "authorship_tag": "ABX9TyOstvekb2RqZobU31GB2FtQ", + "include_colab_link": true + }, + "kernelspec": { + "name": "python3", + "display_name": "Python 3" + }, + "language_info": { + "name": "python" + } + }, + "cells": [ + { + "cell_type": "markdown", + "metadata": { + "id": "view-in-github", + "colab_type": "text" + }, + "source": [ + "\"Open" + ] + }, + { + "cell_type": "markdown", + "source": [ + "" + ], + "metadata": { + "id": "QjHXD27ieTS-" + } + }, + { + "cell_type": "markdown", + "source": [ + "# Solving Soduku problems with SAT\n", + "\n", + "The purpose of this Python notebook is to use investigate using SAT to solve Sudoku problems. \n", + "\n", + "You should have completed the notebook on SAT constructions before attempting this notebook.\n", + "\n", + "You should have completed the notebook on SAT constructions before attempting this notebook. Work through the cells below, running each cell in turn. In various places you will see the words \"TODO\". Follow the instructions at these places and write code to complete the functions.\n", + "\n", + "You can save a local copy of this notebook in your Google account and work through it in Colab (recommended) or you can download the notebook and run it locally using Jupyter notebook or similar. If you are using CoLab, we recommend that turn off AI autocomplete (under cog icon in top-right corner), which will give you the answers and defeat the purpose of the exercise.\n", + "\n", + "A fully working version of this notebook with the complete answers can be found [here](https://colab.research.google.com/github/udlbook/udlbook/blob/main/Trees/SAT_Sudoku_Answers.ipynb).\n", + "\n", + "Contact me at iclimbtreesmail@gmail.com if you find any mistakes or have any suggestions." + ], + "metadata": { + "id": "jtMs90veeZIn" + } + }, + { + "cell_type": "code", + "source": [ + "# Install relevant packages\n", + "!pip install z3-solver\n", + "from z3 import *\n", + "import numpy as np\n", + "import geopandas as gpd\n", + "import matplotlib.pyplot as plt" + ], + "metadata": { + "id": "mF6ngqCses3n" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Now let's define a Sudoku problem. We'll make a 9x9 matrix use zeros to represent unknown values." + ], + "metadata": { + "id": "3A5_7mByYrur" + } + }, + { + "cell_type": "code", + "source": [ + "puzzle = [[0,0,9,4,2,0,0,6,0],\n", + " [0,7,0,9,0,5,3,0,2],\n", + " [5,0,0,0,0,3,0,9,0],\n", + " [0,0,0,8,0,1,0,2,0],\n", + " [2,6,0,0,0,0,0,5,1],\n", + " [0,1,8,2,0,0,4,0,0],\n", + " [3,8,0,0,0,4,0,1,9],\n", + " [0,9,4,0,3,0,6,8,5],\n", + " [0,2,1,0,0,8,0,3,0]]" + ], + "metadata": { + "id": "cvGNbKkf-Qix" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "def expandLine(line):\n", + " return line[0]+line[5:9].join([line[1:5]*2]*3)+line[9:13]\n", + "\n", + "def drawPuzzle(puzzle):\n", + " line0 = expandLine(\"╔═══╤═══╦═══╗\")\n", + " line1 = expandLine(\"║ . │ . ║ . ║\")\n", + " line2 = expandLine(\"╟───┼───╫───╢\")\n", + " line3 = expandLine(\"╠═══╪═══╬═══╣\")\n", + " line4 = expandLine(\"╚═══╧═══╩═══╝\")\n", + "\n", + " symbol = \" 123456789\"\n", + " nums = [ [\"\"]+[symbol[n] for n in row] for row in puzzle ]\n", + " print(line0)\n", + " for r in range(1,9+1):\n", + " print( \"\".join(n+s for n,s in zip(nums[r-1],line1.split(\".\"))) )\n", + " print([line2,line3,line4][(r%9==0)+(r%3==0)])" + ], + "metadata": { + "id": "0EkPFukj_-qc" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "drawPuzzle(puzzle)" + ], + "metadata": { + "id": "CB0QFnLODWTu" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "# Takes a list of z3.Bool variables and returns constraints\n", + "# ensuring that there is exactly one true\n", + "def exactly_one(x):\n", + " return PbEq([(i,1) for i in x],1)\n", + "\n", + "def solve_soduku(puzzle):\n", + " # Create a 9 x 9 x 9 structure containing Boolean variables\n", + " # If position (i,j,k) is true, this means position (i,j) in the puzzle matrix\n", + " # takes color k+1\n", + " x = [[[ z3.Bool(\"x_{%d,%d,%d}\"%((i,j,k))) for k in range(0,9)] for j in range(0,9) ] for i in range(0,9) ]\n", + " # Set up the sat solver\n", + " s = Solver()\n", + "\n", + " # Add constraint one: each position where the entry is already known\n", + " # should be set to true. Don't forget that the indices of x start at zero not one.\n", + " # TODO: Replace this code.\n", + " s.add(x[1][0])\n", + "\n", + "\n", + " # Add constraint two: each position in the matrix can have only one color\n", + " # For fixed i and j, only one value of k can be true\n", + " # TODO: Replace this code.\n", + " s.add(x[1][0])\n", + "\n", + " # Add constraint three: each row of the table can only have each value once\n", + " # TODO: Replace this code.\n", + " s.add(x[1][0])\n", + "\n", + " # Add constraint four: each column of the table can only have each value once\n", + " # TODO: Replace this code.\n", + " s.add(x[1][0])\n", + "\n", + " # Add constraint five: each 3x3 region can only have each value once\n", + " # TODO: Replace this code.\n", + " s.add(x[1][0])\n", + "\n", + " # Check if it's SAT (creates the model)\n", + " sat_result = s.check()\n", + " print(sat_result)\n", + "\n", + " # If it isn't then return\n", + " if sat_result == z3.sat:\n", + " result = s.model()\n", + " x_vals = np.array([[[int(bool(result[z3.Bool(\"x_{%d,%d,%d}\" % (i, j, k))])) for k in range(9)] for j in range(9)] for i in range(9)] )\n", + " solution = np.argmax(x_vals, axis=2) + 1\n", + " drawPuzzle(solution)\n", + " else:\n", + " print(\"No solution\")\n", + "\n" + ], + "metadata": { + "id": "dRmdNKGdZRks" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "# Call the routine to solve the Soduku puzzle\n", + "solve_soduku(puzzle)" + ], + "metadata": { + "id": "0HeFo62NZfBp" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Now let's try it with a more difficult example. Try to solve this yourself and you'll see that it's pretty hard." + ], + "metadata": { + "id": "vL-sDmF7tnxa" + } + }, + { + "cell_type": "code", + "source": [ + "puzzle2 = [[0,5,0,0,0,9,0,8,0],\n", + " [7,0,0,0,0,3,6,0,5],\n", + " [0,0,0,0,6,0,0,1,0],\n", + " [0,0,0,0,0,0,0,6,0],\n", + " [0,1,0,0,3,0,4,0,9],\n", + " [0,0,2,0,0,7,0,0,0],\n", + " [0,9,0,0,4,0,5,0,3],\n", + " [1,0,0,9,0,0,0,0,0],\n", + " [0,0,0,0,0,0,0,0,8]]\n", + "drawPuzzle(puzzle2)\n", + "solve_soduku(puzzle2)" + ], + "metadata": { + "id": "3SWS2QUqtlNI" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Finally, let's modify the last puzzle so it is (non-obviously) impossible to solve. I've just added a 3 to position (3,3) on the grid. It looks innoccuous, but actually makes the puzzle unsolvable." + ], + "metadata": { + "id": "opc4hxI2ugU7" + } + }, + { + "cell_type": "code", + "source": [ + "puzzle3 = [[0,5,0,0,0,9,0,8,0],\n", + " [7,0,0,0,0,3,6,0,5],\n", + " [0,0,3,0,6,0,0,1,0],\n", + " [0,0,0,0,0,0,0,6,0],\n", + " [0,1,0,0,3,0,4,0,9],\n", + " [0,0,2,0,0,7,0,0,0],\n", + " [0,9,0,0,4,0,5,0,3],\n", + " [1,0,0,9,0,0,0,0,0],\n", + " [0,0,0,0,0,0,0,0,8]]\n", + "drawPuzzle(puzzle3)\n", + "solve_soduku(puzzle3)" + ], + "metadata": { + "id": "0lfUKX66ubj0" + }, + "execution_count": null, + "outputs": [] + } + ] +} \ No newline at end of file