diff --git a/Trees/SAT_Graph_Coloring_Answers.ipynb b/Trees/SAT_Graph_Coloring_Answers.ipynb new file mode 100644 index 0000000..8dec5e2 --- /dev/null +++ b/Trees/SAT_Graph_Coloring_Answers.ipynb @@ -0,0 +1,276 @@ +{ + "nbformat": 4, + "nbformat_minor": 0, + "metadata": { + "colab": { + "provenance": [], + "authorship_tag": "ABX9TyOfpzSI63fglgJWohin4iY/", + "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 for graph coloring problems. We'll aim to color a map of the United States in such a way that no two adjacent states have the same color. We'll both aim to find a valid color labelling and to determine the minimum number of colors for which this is possible.\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", + "from itertools import combinations\n", + "import geopandas as gpd\n", + "import matplotlib.pyplot as plt" + ], + "metadata": { + "id": "mF6ngqCses3n" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "First let's download a map of the United States and form a 49x49 matrix representing the adjacencies of the lower 48 states. There will be a one in the matrix if two states are adjacent and a zero otherwise." + ], + "metadata": { + "id": "fMXNLIZGQzby" + } + }, + { + "cell_type": "code", + "source": [ + "# Download map of the US\n", + "!wget https://github.com/udlbook/udlbook/raw/refs/heads/main/Trees/cb_2018_us_state_500k.zip\n", + "!unzip -o cb_2018_us_state_500k.zip\n", + "# Read shape data\n", + "# Read the shapefile into a GeoDataFrame\n", + "try:\n", + " states = gpd.read_file(\"cb_2018_us_state_500k.shp\")\n", + "except FileNotFoundError:\n", + " print(\"Shapefile not found. Please make sure 'cb_2018_us_state_500k.shp' is in the current directory.\")\n", + " exit()\n", + "\n", + "# Reatain just lower 48 states and DC to make it easier to draw\n", + "lower48 = states[~states['NAME'].isin(['Alaska', 'Hawaii', 'American Samoa', 'Virgin Islands', \\\n", + " 'Commonwealth of the Northern Mariana Islands', 'Guam', \\\n", + " 'Puerto Rico', 'United States Virgin Islands', 'District of Columbia'])]\n", + "\n", + "# Reset the index to remove gaps\n", + "lower48 = lower48.reset_index(drop=True)" + ], + "metadata": { + "id": "Xfg3YopGffZn" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "# Get adjacency matrix for remaining 48 states plus DC.\n", + "\n", + "# Get the number of states\n", + "num_states = len(lower48)\n", + "\n", + "# Create an empty adjacency matrix\n", + "adjacency_matrix = np.zeros((num_states, num_states), dtype=int)\n", + "\n", + "# Iterate through pairs of states\n", + "for i in range(num_states):\n", + " for j in range(i + 1, num_states):\n", + " # Check if the geometries of the two states intersect\n", + " if lower48.geometry[i].intersects(lower48.geometry[j]):\n", + " adjacency_matrix[i, j] = 1\n", + " adjacency_matrix[j, i] = 1 # Adjacency matrix is symmetric" + ], + "metadata": { + "id": "W5YOa3-kD04W" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Now let's write a rountine that draws the map given a set of 49 input colors" + ], + "metadata": { + "id": "xi2FRkqpRHmk" + } + }, + { + "cell_type": "code", + "source": [ + "def draw_map(lower48, color_indices):\n", + "\n", + " # Define a list of colors\n", + " colors = ['#316879', '#f47a60', '#7fe7dc', '#ced7d8', '#424b4f', '#773c23', '#aec3cf']\n", + "\n", + " # Assign a random color to each state\n", + " lower48['color'] = [colors[color_indices[i]] for i in range(len(lower48))]\n", + "\n", + " # Create the plot\n", + " fig, ax = plt.subplots(1, 1, figsize=(10, 6))\n", + "\n", + " # Plot the states with the assigned colors\n", + " lower48.plot(color=lower48['color'], cmap=None, categorical=True, legend=False, ax=ax, edgecolor='0.8')\n", + "\n", + " # Customize the plot (optional)\n", + " ax.set_axis_off()\n", + "\n", + " # Display the plot\n", + " plt.show()" + ], + "metadata": { + "id": "F9s4LoceWm1p" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "# Test the drawing routine with random colors\n", + "color_indices = np.random.randint(0, 7, size=48)\n", + "draw_map(lower48, color_indices)" + ], + "metadata": { + "id": "X8GL1sbfSq4z" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Now let's write a routine to color the map in such a way that no two adjacent states have the same color" + ], + "metadata": { + "id": "3A5_7mByYrur" + } + }, + { + "cell_type": "code", + "source": [ + "def exactly_one(x):\n", + " return PbEq([(i,1) for i in x],1)\n", + "\n", + "def graph_coloring(adjacency_matrix, n_colors):\n", + " # Create an n_state by n_color structure (list of lists) of binary variables\n", + " # There will be a 1 in a given position if that state has that particular color\n", + " n_state = adjacency_matrix.shape[0]\n", + " x = [[ z3.Bool(\"x_{%d,%d}\"%((i,j))) for j in range(0,n_colors) ] for i in range(0,n_state) ]\n", + " # Set up the sat solver\n", + " s = Solver()\n", + "\n", + " # Add constraint one: each state can only have one color\n", + " # For each row of the matrix, exactly one variable is true\n", + " for c_state in range(0,n_state):\n", + " s.add(exactly_one(x[c_state]))\n", + "\n", + " # Add constraint two. Two adjacent states cannot have the same color\n", + " # If there is a one in the adjacency matrix at position i,j, then variable\n", + " # x[i, color] and x[j, color] cannot both be true for every color\n", + " for c_state in range(0,n_state):\n", + " for c_neighbor in range(c_state+1,n_state):\n", + " if adjacency_matrix[c_state,c_neighbor]:\n", + " for c_color in range(0,n_colors):\n", + " s.add(Or(Not(x[c_state][c_color]),Not(x[c_neighbor][c_color])))\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}\" % (i, j))])) for j in range(7)] for i in range(48)])\n", + " color_indices = np.argmax(x_vals, axis=1)\n", + " draw_map(lower48, color_indices)\n", + "\n", + "\n", + "" + ], + "metadata": { + "id": "dRmdNKGdZRks" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "# Call the routine to compute the graph coloring with seven colors\n", + "graph_coloring(adjacency_matrix, 7)" + ], + "metadata": { + "id": "0HeFo62NZfBp" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "# TODO Find the minimum number of colors needed for a valid solution\n", + "# Add some code here" + ], + "metadata": { + "id": "Qe629Lui0nlW" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "You can find more about the minimum number of colors required for a planar graph like this in this [Wikipedia page](https://en.wikipedia.org/wiki/Four_color_theorem)" + ], + "metadata": { + "id": "RPkY-lHh11i_" + } + } + ] +} \ No newline at end of file