diff --git a/Trees/SAT_Sudoku_Answers.ipynb b/Trees/SAT_Sudoku_Answers.ipynb new file mode 100644 index 0000000..8c045ad --- /dev/null +++ b/Trees/SAT_Sudoku_Answers.ipynb @@ -0,0 +1,435 @@ +{ + "nbformat": 4, + "nbformat_minor": 0, + "metadata": { + "colab": { + "provenance": [], + "authorship_tag": "ABX9TyMDkDz3RrsH0nJVTdsejhO7", + "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": [ + "# Graph coloring\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 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.\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", + "colab": { + "base_uri": "https://localhost:8080/" + }, + "outputId": "fad1115b-b146-46bc-b298-7c0885fe75ac" + }, + "execution_count": 1, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "Collecting z3-solver\n", + " Downloading z3_solver-4.14.1.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.metadata (602 bytes)\n", + "Downloading z3_solver-4.14.1.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (29.5 MB)\n", + "\u001b[2K \u001b[90m━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━\u001b[0m \u001b[32m29.5/29.5 MB\u001b[0m \u001b[31m17.6 MB/s\u001b[0m eta \u001b[36m0:00:00\u001b[0m\n", + "\u001b[?25hInstalling collected packages: z3-solver\n", + "Successfully installed z3-solver-4.14.1.0\n" + ] + } + ] + }, + { + "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": 2, + "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": 3, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "drawPuzzle(puzzle)" + ], + "metadata": { + "colab": { + "base_uri": "https://localhost:8080/" + }, + "id": "CB0QFnLODWTu", + "outputId": "3698caa2-e0a2-466a-a542-5e141d7b6bce" + }, + "execution_count": 4, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n", + "║ │ │ 9 ║ 4 │ 2 │ ║ │ 6 │ ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ 7 │ ║ 9 │ │ 5 ║ 3 │ │ 2 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 5 │ │ ║ │ │ 3 ║ │ 9 │ ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ │ │ ║ 8 │ │ 1 ║ │ 2 │ ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 2 │ 6 │ ║ │ │ ║ │ 5 │ 1 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ 1 │ 8 ║ 2 │ │ ║ 4 │ │ ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ 3 │ 8 │ ║ │ │ 4 ║ │ 1 │ 9 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ 9 │ 4 ║ │ 3 │ ║ 6 │ 8 │ 5 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ 2 │ 1 ║ │ │ 8 ║ │ 3 │ ║\n", + "╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n" + ] + } + ] + }, + { + "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\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.\n", + " for i in range(0,9):\n", + " for j in range(0,9):\n", + " if puzzle[i][j] > 0:\n", + " s.add(x[i][j][puzzle[i][j]-1] == True)\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", + " for i in range(0,9):\n", + " for j in range(0,9):\n", + " s.add(exactly_one([x[i][j][k] for k in range(0,9)]))\n", + "\n", + " # Add constraint three: each row of the table can only have each value once\n", + " for i in range(0,9):\n", + " for k in range(0,9):\n", + " s.add(exactly_one([x[i][j][k] for j in range(0,9)]))\n", + "\n", + " # Add constraint four: each column of the table can only have each value once\n", + " for j in range(0,9):\n", + " for k in range(0,9):\n", + " s.add(exactly_one([x[i][j][k] for i in range(0,9)]))\n", + "\n", + " # Add constraint five: each 3x3 region can only have each value once\n", + " for i in range(0,9,3):\n", + " for j in range(0,9,3):\n", + " for k in range(0,9):\n", + " s.add(exactly_one([x[i+a][j+b][k] for a in range(0,3) for b in range(0,3)]))\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": 23, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "# Call the routine to solve the Soduku puzzle\n", + "solve_soduku(puzzle)" + ], + "metadata": { + "id": "0HeFo62NZfBp", + "colab": { + "base_uri": "https://localhost:8080/" + }, + "outputId": "8840695c-8ce0-4ce1-93ef-d68d1c7098ed" + }, + "execution_count": 24, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "sat\n", + "╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n", + "║ 1 │ 3 │ 9 ║ 4 │ 2 │ 7 ║ 5 │ 6 │ 8 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 8 │ 7 │ 6 ║ 9 │ 1 │ 5 ║ 3 │ 4 │ 2 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 5 │ 4 │ 2 ║ 6 │ 8 │ 3 ║ 1 │ 9 │ 7 ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ 4 │ 5 │ 3 ║ 8 │ 7 │ 1 ║ 9 │ 2 │ 6 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 2 │ 6 │ 7 ║ 3 │ 4 │ 9 ║ 8 │ 5 │ 1 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 9 │ 1 │ 8 ║ 2 │ 5 │ 6 ║ 4 │ 7 │ 3 ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ 3 │ 8 │ 5 ║ 7 │ 6 │ 4 ║ 2 │ 1 │ 9 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 7 │ 9 │ 4 ║ 1 │ 3 │ 2 ║ 6 │ 8 │ 5 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 6 │ 2 │ 1 ║ 5 │ 9 │ 8 ║ 7 │ 3 │ 4 ║\n", + "╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n" + ] + } + ] + }, + { + "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": { + "colab": { + "base_uri": "https://localhost:8080/" + }, + "id": "3SWS2QUqtlNI", + "outputId": "8c7419ff-70b2-4322-81c0-2f8d8727de72" + }, + "execution_count": 32, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n", + "║ │ 5 │ ║ │ │ 9 ║ │ 8 │ ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 7 │ │ ║ │ │ 3 ║ 6 │ │ 5 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ │ ║ │ 6 │ ║ │ 1 │ ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ │ │ ║ │ │ ║ │ 6 │ ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ 1 │ ║ │ 3 │ ║ 4 │ │ 9 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ │ 2 ║ │ │ 7 ║ │ │ ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ │ 9 │ ║ │ 4 │ ║ 5 │ │ 3 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 1 │ │ ║ 9 │ │ ║ │ │ ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ │ ║ │ │ ║ │ │ 8 ║\n", + "╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n", + "sat\n", + "╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n", + "║ 6 │ 5 │ 1 ║ 7 │ 2 │ 9 ║ 3 │ 8 │ 4 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 7 │ 8 │ 9 ║ 4 │ 1 │ 3 ║ 6 │ 2 │ 5 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 3 │ 2 │ 4 ║ 8 │ 6 │ 5 ║ 9 │ 1 │ 7 ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ 9 │ 3 │ 5 ║ 1 │ 8 │ 4 ║ 7 │ 6 │ 2 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 8 │ 1 │ 7 ║ 2 │ 3 │ 6 ║ 4 │ 5 │ 9 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 4 │ 6 │ 2 ║ 5 │ 9 │ 7 ║ 8 │ 3 │ 1 ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ 2 │ 9 │ 8 ║ 6 │ 4 │ 1 ║ 5 │ 7 │ 3 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 1 │ 7 │ 3 ║ 9 │ 5 │ 8 ║ 2 │ 4 │ 6 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 5 │ 4 │ 6 ║ 3 │ 7 │ 2 ║ 1 │ 9 │ 8 ║\n", + "╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n" + ] + } + ] + }, + { + "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": { + "colab": { + "base_uri": "https://localhost:8080/" + }, + "id": "0lfUKX66ubj0", + "outputId": "e74941c8-addd-46fd-d908-34b0d975fd71" + }, + "execution_count": 34, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n", + "║ │ 5 │ ║ │ │ 9 ║ │ 8 │ ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 7 │ │ ║ │ │ 3 ║ 6 │ │ 5 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ │ 3 ║ │ 6 │ ║ │ 1 │ ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ │ │ ║ │ │ ║ │ 6 │ ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ 1 │ ║ │ 3 │ ║ 4 │ │ 9 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ │ 2 ║ │ │ 7 ║ │ │ ║\n", + "╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n", + "║ │ 9 │ ║ │ 4 │ ║ 5 │ │ 3 ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ 1 │ │ ║ 9 │ │ ║ │ │ ║\n", + "╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n", + "║ │ │ ║ │ │ ║ │ │ 8 ║\n", + "╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n", + "unsat\n", + "No solution\n" + ] + } + ] + } + ] +} \ No newline at end of file