diff --git a/Trees/SAT_Construction2_Answers.ipynb b/Trees/SAT_Construction2_Answers.ipynb new file mode 100644 index 0000000..bc73e2a --- /dev/null +++ b/Trees/SAT_Construction2_Answers.ipynb @@ -0,0 +1,261 @@ +{ + "nbformat": 4, + "nbformat_minor": 0, + "metadata": { + "colab": { + "provenance": [], + "authorship_tag": "ABX9TyNVGP04pippHj/aR+N+9Vyv", + "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": "jv83sxEU2Ig0" + } + }, + { + "cell_type": "markdown", + "source": [ + "# SAT Constructions\n", + "\n", + "The purpose of this Python notebook is to investigate the SAT construction that tests if a graph is connected.\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": "IsBSW40O20Hv" + } + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": { + "id": "WZYb15hc19es" + }, + "outputs": [], + "source": [ + "!pip install z3-solver\n", + "from z3 import *\n", + "import numpy as np\n", + "from itertools import combinations" + ] + }, + { + "cell_type": "markdown", + "source": [ + "# Connected components\n", + "\n", + "Finally, let's develop a construction that tells us if the elements of an undirected graph are connected. Consider the two adjacency matrices:\n", + "\n", + "\\begin{equation}\n", + "A_1 = \\begin{bmatrix}1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 \\\\\n", + " 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 \\\\\n", + " 0 & 1 & 1 & 1 & 0 & 0 & 0 & 0 \\\\\n", + " 0 & 0 & 1 & 1 & 1 & 0 & 0 & 0 \\\\\n", + " 0 & 0 & 0 & 1 & 1 & 1 & 0 & 0 \\\\\n", + " 0 & 0 & 0 & 0 & 1 & 1 & 1 & 0 \\\\\n", + " 0 & 0 & 0 & 0 & 0 & 1 & 1 & 1 \\\\\n", + " 0 & 0 & 0 & 0 & 0 & 0 & 1 & 1 \\\\\n", + " \\end{bmatrix} \\quad\\quad\n", + " A_2 = \\begin{bmatrix}1 & 1 & 0 & 1 & 0 & 0 & 0 & 0 \\\\\n", + " 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 \\\\\n", + " 0 & 1 & 1 & 1 & 0 & 0 & 0 & 0 \\\\\n", + " 1 & 0 & 1 & 1 & 1 & 0 & 0 & 0 \\\\\n", + " 0 & 0 & 0 & 1 & 1 & 1 & 0 & 0 \\\\\n", + " 0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 \\\\\n", + " 0 & 0 & 0 & 0 & 0 & 0 & 1 & 1 \\\\\n", + " 0 & 0 & 0 & 0 & 0 & 0 & 1 & 1 \\\\\n", + " \\end{bmatrix}\n", + "\\end{equation}\n", + "\n", + "Each matrix represents the edges in a graph containing eight nodes. Elements $(i,j)$ and $(j,i)$ will be set to one if there is an edge between nodes $i$ and $j$. The diagonal elements are all set to one.\n", + "\n", + "For matrix $A_{1}$ the nodes are all connected; node 1 connects to node 2, which connects to node 3, and so on up to node 8. \n", + "\n", + "For matrix $A_{2}$ however, the nodes are not all connected. Nodes 7 and 8 are connected to each other but not connected any of the other nodes.\n" + ], + "metadata": { + "id": "CZQygtit0D9Q" + } + }, + { + "cell_type": "markdown", + "source": [ + "We can test for the connectivity of the graph implied by an $8\\times 8$ matrix $\\mathbf{A}$ by computing new adjacency matrices $\\mathbf{B},\\mathbf{C},\\mathbf{D}$ where:\n", + "\n", + "$$\\begin{aligned}\n", + "B_{ij} &\\Leftrightarrow \\bigvee_k (A_{ik} \\land A_{kj})\\\\\n", + "C_{ij} &\\Leftrightarrow \\bigvee_k (B_{ik} \\land B_{kj})\\\\\n", + "D_{ij} &\\Leftrightarrow \\bigvee_k (C_{ik} \\land C_{kj})\n", + "\\end{aligned}\n", + "$$\n", + "\n", + "and then enforcing the constraint that the first row of $\\mathbf{D}$ contains all true elements:\n", + "\n", + "$$ \\bigvee_k D_{0,k}$$\n", + "\n", + "In general, if the initial matrix $\\mathbf{A}$ is of size $N\\times N$, we will need to compute $\\log_2[N]$ intermediate matrices $\\mathbf{B},\\mathbf{C},\\mathbf{D}$." + ], + "metadata": { + "id": "2brsB9m54aGo" + } + }, + { + "cell_type": "markdown", + "source": [ + "Now let's write a SAT routine to check if an adjacency matrix represents a fully-connected graph" + ], + "metadata": { + "id": "TxctcAsX8rh0" + } + }, + { + "cell_type": "code", + "source": [ + "def is_fully_connected(s, adjacency):\n", + " # Size of the adjacency matrix\n", + " n_components = len(adjacency)\n", + " # We'll construct a N x N x log[N] array of variables\n", + " # The NxN variables in the first layer represent A, the variables in the second layer represent B and so on\n", + " n_layers = math.ceil(math.log(n_components,2))+1\n", + " connected = [[[ z3.Bool(\"conn_{%d,%d,%d}\"%((i,j,n))) for n in range(0, n_layers)] for j in range(0, n_components) ] for i in range(0, n_components) ]\n", + "\n", + " # Constraint 1\n", + " # The value in the top layer of the connected structure is equal to the adjacency matrix\n", + " for i in range(n_components):\n", + " for j in range(n_components):\n", + " s.add(connected[i][j][0]==adjacency[i][j])\n", + "\n", + " # Constraint 2\n", + " # Value at position [i,j] in layer n is true if there is a k such that position[i,k] and positions [k,j] in layer n-1 are true\n", + " for n in range(1,n_layers):\n", + " for i in range(n_components):\n", + " for j in range(n_components):\n", + " matrix_entry_ij = False\n", + " for k in range(n_components):\n", + " matrix_entry_ij = Or(matrix_entry_ij, And(connected[i][k][n-1],connected[k][j][n-1]))\n", + " s.add(connected[i][j][n]==matrix_entry_ij)\n", + "\n", + " # Constraint 3 -- any row of column of the matrix should be full of ones at the end (everything is connected)\n", + " for i in range(n_components):\n", + " s.add(connected[i][0][n_layers-1])\n", + "\n", + " return s" + ], + "metadata": { + "id": "JpfVC-Rg0LiC" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Finally, let's write a routine that tests the adjacency of the two matrices above using a SAT solver." + ], + "metadata": { + "id": "slbVVZH6-_Jl" + } + }, + { + "cell_type": "code", + "source": [ + "def test_is_fully_connected(A):\n", + " # Set up the SAT solver\n", + " s = Solver()\n", + "\n", + " # Convert the input matrix to z3 Boolean values\n", + " n_components = A.shape[0]\n", + " adjacency= [[ z3.Bool(\"a_{%d,%d}\"%((i,j))) for j in range(0, n_components) ] for i in range(0, n_components) ]\n", + " for i in range(n_components):\n", + " for j in range(n_components):\n", + " if A[i,j]!=0:\n", + " s.add(adjacency[i][j])\n", + " else:\n", + " s.add(Not(adjacency[i][j]))\n", + "\n", + " # Run the routine\n", + " s = is_fully_connected(s, adjacency)\n", + "\n", + " # Check if it's SAT (creates the model)\n", + " sat_result = s.check()\n", + " print(sat_result)\n", + "\n", + " # If it was SAT then print out the layers of the 3D structure\n", + " if sat_result == z3.sat:\n", + " result = s.model()\n", + " c_vals = np.array([[[int(bool(result[z3.Bool(\"conn_{%d,%d,%d}\" % (i, j,n))])) for n in range(0, n_components-1)] for j in range(0,n_components) ] for i in range(0,n_components) ] )\n", + " for n in range(math.ceil(math.log(n_components,2))+1):\n", + " print(\"Layer:\",n)\n", + " print(c_vals[:,:,n])" + ], + "metadata": { + "id": "0veuGhg_--EJ" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "A1 = np.array([[1, 1, 0, 0, 0, 0, 0, 0],\n", + " [1, 1, 1, 0, 0, 0, 0, 0],\n", + " [0, 1, 1, 1, 0, 0, 0, 0],\n", + " [0, 0, 1, 1, 1, 0, 0, 0],\n", + " [0, 0, 0, 1, 1, 1, 0, 0],\n", + " [0, 0, 0, 0, 1, 1, 1, 0],\n", + " [0, 0, 0, 0, 0, 1, 1, 1],\n", + " [0, 0, 0, 0, 0, 0, 1, 1]])\n", + "test_is_fully_connected(A1)" + ], + "metadata": { + "id": "rk83toMaAkQX" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "A2 = np.array([[1, 1, 0, 1, 0, 0, 0, 0],\n", + " [1, 1, 1, 0, 0, 0, 0, 0],\n", + " [0, 1, 1, 1, 0, 0, 0, 0],\n", + " [1, 0, 1, 1, 1, 0, 0, 0],\n", + " [0, 0, 0, 1, 1, 1, 0, 0],\n", + " [0, 0, 0, 0, 1, 1, 0, 0],\n", + " [0, 0, 0, 0, 0, 0, 1, 1],\n", + " [0, 0, 0, 0, 0, 0, 1, 1]])\n", + "test_is_fully_connected(A2)" + ], + "metadata": { + "id": "DRzo_XrCAlrz" + }, + "execution_count": null, + "outputs": [] + } + ] +} \ No newline at end of file