diff --git a/Trees/SAT_Construction_Answers.ipynb b/Trees/SAT_Construction_Answers.ipynb index 823db5a..99da5d5 100644 --- a/Trees/SAT_Construction_Answers.ipynb +++ b/Trees/SAT_Construction_Answers.ipynb @@ -4,7 +4,7 @@ "metadata": { "colab": { "provenance": [], - "authorship_tag": "ABX9TyMjeWJ3+JkP3KO4xuarMyeL", + "authorship_tag": "ABX9TyNalp5KWVPvcXsJJ4jQvQ5U", "include_colab_link": true }, "kernelspec": { @@ -40,7 +40,7 @@ "source": [ "# SAT Constructions\n", "\n", - "The purpose of this Python notebook is to use investigate SAT constructions that impose constraints on sets of variables. We'll build constructions for ensuring all of the variables are the same, that only one of the variables is true, that at leats $K$ of the variables are true, that fewer than $K$ of the variables are true and that exactly $K$ of the variables are true.\n", + "The purpose of this Python notebook is to investigate SAT constructions that impose constraints on sets of variables. We'll build constructions for ensuring all of the variables are the same, that only one of the variables is true, that at leats $K$ of the variables are true, that fewer than $K$ of the variables are true and that exactly $K$ of the variables are true.\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", @@ -581,409 +581,6 @@ }, "execution_count": null, "outputs": [] - }, - { - "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", - "\n", - "We can test this by multiplying any adjacency matrix of size $N\\times N$ by itself $N-1$ times (or more). If the resulting matrix contains all non-zero elements then the graph was fully connected. If there are any zeros, then the graph is not fully connected. Let's try that for these two matrices.\n" - ], - "metadata": { - "id": "CZQygtit0D9Q" - } - }, - { - "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", - "\n", - "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", - "\n", - "\n", - "print(\"Matrix A1 is fully connected. Product does not contain any zeros :\\n\\n\",A1@A1@A1@A1@A1@A1@A1)\n", - "print(\"\\nMatrix A2 is not fully connected. Product contains zeros :\\n\\n\",A2@A2@A2@A2@A2@A2@A2)" - ], - "metadata": { - "colab": { - "base_uri": "https://localhost:8080/" - }, - "id": "ywLO1nan2_6K", - "outputId": "4704aab6-a155-4bd3-857d-d4a6c3b38947" - }, - "execution_count": null, - "outputs": [ - { - "output_type": "stream", - "name": "stdout", - "text": [ - "Matrix A1 is fully connected. Product does not contain any zeros :\n", - "\n", - " [[127 196 189 133 70 27 7 1]\n", - " [196 316 329 259 160 77 28 7]\n", - " [189 329 386 356 266 161 77 27]\n", - " [133 259 356 393 357 266 160 70]\n", - " [ 70 160 266 357 393 356 259 133]\n", - " [ 27 77 161 266 356 386 329 189]\n", - " [ 7 28 77 160 259 329 316 196]\n", - " [ 1 7 27 70 133 189 196 127]]\n", - "\n", - "Matrix A2 is not fully connected. Product contains zeros :\n", - "\n", - " [[ 652 609 651 800 441 191 0 0]\n", - " [ 609 575 609 728 382 154 0 0]\n", - " [ 651 609 652 800 441 191 0 0]\n", - " [ 800 728 800 1016 609 287 0 0]\n", - " [ 441 382 441 609 421 227 0 0]\n", - " [ 191 154 191 287 227 134 0 0]\n", - " [ 0 0 0 0 0 0 64 64]\n", - " [ 0 0 0 0 0 0 64 64]]\n" - ] - } - ] - }, - { - "cell_type": "markdown", - "source": [ - "In fact we could do this a bit more efficiently, by first calculating $B = A^2$ and then computing $C = B^2 = A^4$ and finally $D=C^2 = A^8$. In this way, we only need $\\log[N]$ multiplications to check the graph is connected." - ], - "metadata": { - "id": "SRQTzwSn4zFD" - } - }, - { - "cell_type": "code", - "source": [ - "B1 = A1@A1\n", - "C1 = B1@B1\n", - "D1 = C1@C1\n", - "print(\"Matrix A1 is fully connected. Product does not contain any zeros :\\n\\n\",D1)\n", - "\n", - "B2 = A2@A2\n", - "C2 = B2@B2\n", - "D2 = C2@C2\n", - "print(\"\\nMatrix A2 is not fully connected. Product contains zeros :\\n\\n\",D2)" - ], - "metadata": { - "colab": { - "base_uri": "https://localhost:8080/" - }, - "id": "xVbt1Fud61tG", - "outputId": "15b4e5ce-47ef-474c-9abc-455388616a75" - }, - "execution_count": null, - "outputs": [ - { - "output_type": "stream", - "name": "stdout", - "text": [ - "Matrix A1 is fully connected. Product does not contain any zeros :\n", - "\n", - " [[ 323 512 518 392 230 104 35 8]\n", - " [ 512 841 904 748 496 265 112 35]\n", - " [ 518 904 1071 1008 783 504 265 104]\n", - " [ 392 748 1008 1106 1016 783 496 230]\n", - " [ 230 496 783 1016 1106 1008 748 392]\n", - " [ 104 265 504 783 1008 1071 904 518]\n", - " [ 35 112 265 496 748 904 841 512]\n", - " [ 8 35 104 230 392 518 512 323]]\n", - "\n", - "Matrix A2 is not fully connected. Product contains zeros :\n", - "\n", - " [[2061 1912 2060 2544 1432 632 0 0]\n", - " [1912 1793 1912 2328 1264 536 0 0]\n", - " [2060 1912 2061 2544 1432 632 0 0]\n", - " [2544 2328 2544 3225 1912 896 0 0]\n", - " [1432 1264 1432 1912 1257 648 0 0]\n", - " [ 632 536 632 896 648 361 0 0]\n", - " [ 0 0 0 0 0 0 128 128]\n", - " [ 0 0 0 0 0 0 128 128]]\n" - ] - } - ] - }, - { - "cell_type": "markdown", - "source": [ - "Obviously, we are working in the world of Boolean variables, so we cannot do full matrix multiplication, but we there is a binary equivalent of matrix multiplication which use AND and OR operations instead of multiplications and additions, respectively. To make this happen, we just define the matrices as boolean and multiply matrices together using the dot product operator between the matrix transpose and itself $\\textrm{dot}[A^T, A]$" - ], - "metadata": { - "id": "2brsB9m54aGo" - } - }, - { - "cell_type": "code", - "source": [ - "A1Bool = A1.astype(bool)\n", - "B1 = np.dot(A1Bool.T, A1Bool)\n", - "C1 = np.dot(B1.T, B1)\n", - "D1 = np.dot(C1.T, C1)\n", - "\n", - "print(\"Matrix A1 is fully connected. Product does not contain any zeros :\\n\\n\",D1)\n", - "\n", - "A2Bool = A2.astype(bool)\n", - "B2 = np.dot(A2Bool.T, A2Bool)\n", - "C2 = np.dot(B2.T, B2)\n", - "D2 = np.dot(C2.T, C2)\n", - "print(\"\\nMatrix A2 is not fully connected. Product contains false values :\\n\\n\",D2)" - ], - "metadata": { - "colab": { - "base_uri": "https://localhost:8080/" - }, - "id": "o_jvXGDV4Wer", - "outputId": "da2b933d-27df-40d9-88cb-de2a4a28b032" - }, - "execution_count": null, - "outputs": [ - { - "output_type": "stream", - "name": "stdout", - "text": [ - "\n", - "Matrix A1 is fully connected. Product does not contain any zeros :\n", - "\n", - " [[ True True True True True True True True]\n", - " [ True True True True True True True True]\n", - " [ True True True True True True True True]\n", - " [ True True True True True True True True]\n", - " [ True True True True True True True True]\n", - " [ True True True True True True True True]\n", - " [ True True True True True True True True]\n", - " [ True True True True True True True True]]\n", - "Matrix A2 is not fully connected. Product contains false values :\n", - "\n", - " [[ True True True True True True False False]\n", - " [ True True True True True True False False]\n", - " [ True True True True True True False False]\n", - " [ True True True True True True False False]\n", - " [ True True True True True True False False]\n", - " [ True True True True True True False False]\n", - " [False False False False False False True True]\n", - " [False False False False False False True True]]\n" - ] - } - ] - }, - { - "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 value at position [i,j] of the binary matrix product of layer n-1 with itself\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": [ - "test_is_fully_connected(A1)" - ], - "metadata": { - "colab": { - "base_uri": "https://localhost:8080/" - }, - "id": "rk83toMaAkQX", - "outputId": "75fe712d-1565-4509-9a2e-06e2bea19971" - }, - "execution_count": null, - "outputs": [ - { - "output_type": "stream", - "name": "stdout", - "text": [ - "sat\n", - "Layer: 0\n", - "[[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", - "Layer: 1\n", - "[[1 1 1 0 0 0 0 0]\n", - " [1 1 1 1 0 0 0 0]\n", - " [1 1 1 1 1 0 0 0]\n", - " [0 1 1 1 1 1 0 0]\n", - " [0 0 1 1 1 1 1 0]\n", - " [0 0 0 1 1 1 1 1]\n", - " [0 0 0 0 1 1 1 1]\n", - " [0 0 0 0 0 1 1 1]]\n", - "Layer: 2\n", - "[[1 1 1 1 1 0 0 0]\n", - " [1 1 1 1 1 1 0 0]\n", - " [1 1 1 1 1 1 1 0]\n", - " [1 1 1 1 1 1 1 1]\n", - " [1 1 1 1 1 1 1 1]\n", - " [0 1 1 1 1 1 1 1]\n", - " [0 0 1 1 1 1 1 1]\n", - " [0 0 0 1 1 1 1 1]]\n", - "Layer: 3\n", - "[[1 1 1 1 1 1 1 1]\n", - " [1 1 1 1 1 1 1 1]\n", - " [1 1 1 1 1 1 1 1]\n", - " [1 1 1 1 1 1 1 1]\n", - " [1 1 1 1 1 1 1 1]\n", - " [1 1 1 1 1 1 1 1]\n", - " [1 1 1 1 1 1 1 1]\n", - " [1 1 1 1 1 1 1 1]]\n" - ] - } - ] - }, - { - "cell_type": "code", - "source": [ - "test_is_fully_connected(A2)" - ], - "metadata": { - "colab": { - "base_uri": "https://localhost:8080/" - }, - "id": "DRzo_XrCAlrz", - "outputId": "1afa9bfb-8ce0-4c9b-bdd6-20e3aed5e128" - }, - "execution_count": null, - "outputs": [ - { - "output_type": "stream", - "name": "stdout", - "text": [ - "unsat\n" - ] - } - ] } ] } \ No newline at end of file