diff --git a/Trees/SAT_Construction_Answers.ipynb b/Trees/SAT_Construction_Answers.ipynb new file mode 100644 index 0000000..9f97ecf --- /dev/null +++ b/Trees/SAT_Construction_Answers.ipynb @@ -0,0 +1,572 @@ +{ + "nbformat": 4, + "nbformat_minor": 0, + "metadata": { + "colab": { + "provenance": [], + "authorship_tag": "ABX9TyPLe8YcIZiEqqIljGaiTGMy", + "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 use investigate SAT constructions that\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": [ + "# Same\n", + "\n", + "Let's write a subroutine that returns a Boolean logic formula that constrains $n$ variables to be the same.\n", + "\n", + "$$ \\textrm{Same}[x_{1},x_{2},x_{3},\n", + "\\ldots x_{n}]:= (x_{1}\\land x_{2}\\land x_{3},\\ldots,x_n)\\lor(\\overline{x}_{1}\\land \\overline{x}_{2}\\land \\overline{x}_{3},\\ldots,\\overline{x}_n).$$" + ], + "metadata": { + "id": "aVj9RmuB3ZWJ" + } + }, + { + "cell_type": "markdown", + "source": [ + "First let's define the variables. We'll choose $n=10$" + ], + "metadata": { + "id": "Amv5G3VR3zIJ" + } + }, + { + "cell_type": "code", + "source": [ + "n=10\n", + "x = [ z3.Bool(\"x_{i}\".format(i=i)) for i in range(0,n) ]\n", + "print(x)" + ], + "metadata": { + "id": "J-y3uhTs-LU7" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Now let's write the main routine. We can make use of the fact that the Z3 command 'Or' which combines together a list of literals with Or operations." + ], + "metadata": { + "id": "4pY5yiDo-esv" + } + }, + { + "cell_type": "code", + "source": [ + "# Routine that returns the SAT construction (a Boolean logic formula) for all literals in x being the same.\n", + "def same(x):\n", + " return Or(And(x), And([Not(xi) for xi in x]))" + ], + "metadata": { + "id": "f0esE71E94fm" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Finally, let's test that our routine works. Here's generic routine that evaluates a vector of concrete values against a provided Boolean logic formula\n" + ], + "metadata": { + "id": "EWTuxEvrAfnK" + } + }, + { + "cell_type": "code", + "source": [ + "def check_expression(x, formula, literals):\n", + " # Create the solver\n", + " s = Solver()\n", + " # Add the constraint\n", + " s.add(formula(x))\n", + " # Add the literals\n", + " for i,literal in enumerate(literals):\n", + " if literal:\n", + " s.add(x[i])\n", + " else:\n", + " s.add(Not(x[i]))\n", + " # Check if it's SAT (creates the model)\n", + " sat_result = s.check()\n", + " if(sat_result==sat):\n", + " print(\"True\")\n", + " else:\n", + " print(\"False\")" + ], + "metadata": { + "id": "vY5CD6lRArNP" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "check_expression(x, same, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, same, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, same, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, same, [True,True,True,True,True,True,True,True,True,True])" + ], + "metadata": { + "id": "Q3VMIDqfHEei" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "# Exactly One\n", + "\n", + "Now let's write a subroutine that returns a Boolean logic formula that is true when only one of the provided variables are the same.\n", + "\n", + "First, we write a formula that ensures at least one of the variables is true:\n", + "\n", + "$$\\textrm{AtLeastOne}[x_1,x_2,x_3]:= x_{1}\\lor x_{2} \\lor x_{3}, \\ldots, x_{n}.$$\n", + "\n", + "Then, we write a formula that ensures that no more than one is true. For each possible pair of literals, we ensure that they are not both true:\n", + "\n", + "$$\\textrm{NoMoreThanOne}[x_{1},x_{2},x_{3}]:= \\lnot (x_{1}\\land x_{2}) \\land \\lnot (x_{1}\\land x_{3}),\\ldots, \\land \\lnot (x_{n-1}\\land x_{n}) $$\n", + "\n", + "Finally, we **AND** together these two formulae:\n", + "\n", + "$$\\textrm{ExactlyOne}[x_1,x_2,x_3,\\ldots, x_n] = \\textrm{AtLeastOne}[x_1,x_2,x_3, \\ldots, x_N]\\land\\textrm{NoMoreThanOne}[x_1,x_2,x_3, \\ldots x_n]$$\n", + "\n", + "You might want to use the function \"combinations\" from itertools (imported above). Example usage:" + ], + "metadata": { + "id": "0IIRG5ZWIZV6" + } + }, + { + "cell_type": "code", + "source": [ + "test = [ z3.Bool(\"x_{i}\".format(i=i)) for i in range(0,4) ]\n", + "for comb in combinations(test, 2):\n", + " print(comb[0], comb[1])" + ], + "metadata": { + "id": "joeZiDT3LV-r" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "def at_least_one(x):\n", + " return Or(x)\n", + "\n", + "def no_more_than_one(x):\n", + " for comb in combinations(x, 2):\n", + " clauses = And([clauses, Or([Not(comb[0]), Not(comb[1])]) ])\n", + " return clauses\n", + "\n", + "def exactly_one(x):\n", + " return And(at_least_one(x), no_more_than_one(x))" + ], + "metadata": { + "id": "C0HGBOjI99Ex" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Let's test if this works:" + ], + "metadata": { + "id": "2Y_1zYOZIoZI" + } + }, + { + "cell_type": "code", + "source": [ + "check_expression(x, at_least_one, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, at_least_one, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, at_least_one, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, at_least_one, [True,True,True,True,True,True,True,True,True,True])" + ], + "metadata": { + "id": "31gqasHnM3c3" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "# At least K\n", + "\n", + "Finally, we'll build the construction that ensures that there at at least K elements that are true in a vector of length n.\n", + "\n", + "This one is a bit more complicated. We construct an NxK matrix of new literals, lables $r_{n,k}$ Then we add the following constraints.\n", + "\n", + "1. Top left element $r_{0,0}$ is the first data element\n", + "\n", + "$$ r_{00} \\Leftrightarrow x_{1}$$\n", + "\n", + "2. Remaining elements $r_{0,1:}$ must be false\n", + "\n", + "$$ \\overline{r}_{0,j} \\quad\\quad \\forall j\\in\\{1,2,\\ldots k-1\\}$$\n", + "\n", + "3. Remaining elements $r_{i,0}$ in first column are true where x_i is true\n", + "\n", + "$$x_i \\Rightarrow r_{i,0} \\quad\\quad \\forall i\\in\\{1,2,\\ldots n-1\\}$$\n", + "\n", + "4. For rows 1:n-1, if the element above is true, this must be true\n", + "\n", + "$$ r_{i-1,j} \\Rightarrow r_{i,j}\\quad\\quad \\quad\\quad \\forall i\\in\\{1,2,\\ldots n-1\\}, j\\in\\{0,1,\\ldots,k-1\\}$$\n", + "\n", + "5. If x is true for this row and the element above and to the left is true then set this element to true.\n", + "\n", + "$$ (x_i \\land r_{i-1,j-1})\\Rightarrow r_{i,j} \\quad\\quad \\forall i\\in\\{1,2,\\ldots n-1\\}, j\\in\\{1,2,\\ldots,k-1\\} $$\n", + "\n", + "6. If x is false for this row and the element above is false then set to false\n", + "\n", + "$$ (\\overline{x}_{i} \\land \\overline{r}_{i-1,j}) \\Rightarrow \\overline{r}_{i,j} \\quad\\quad \\forall i\\in\\{1,2,\\ldots n-1\\}, j\\in\\{1,2,\\ldots,k-1\\} $$\n", + "\n", + "7. if x is false for this row and the element above and to the left is false then set to false:\n", + "\n", + "$$ (\\overline{x}_i \\land \\overline{r}_{i-1,j-1})\\Rightarrow \\overline{r}_{i,j} \\quad\\quad \\forall i\\in\\{1,2,\\ldots n-1\\}, j\\in\\{1,2,\\ldots,k-1\\} $$\n", + "\n", + "8. The bottom-right element of r must be true\n", + "\n", + "$$ r_{n-1,k-1}$$" + ], + "metadata": { + "id": "MJqWOMBsQrCI" + } + }, + { + "cell_type": "code", + "source": [ + "def at_least_k(x, k):\n", + " # Create nxk table of literals r_{i,j}\n", + " n = len(x) ;\n", + " r = [[ z3.Bool(\"r_{%d,%d}\"%((i,j))) for j in range(0,k) ] for i in range(0,n) ]\n", + "\n", + " #1. Top left element $r_{0,0}$ is the first data element\n", + "\n", + " clauses = (r[0][0] == x[0])\n", + "\n", + " #2. Remaining elements $r_{0,1:}$ must be false\n", + "\n", + " clauses = And(clauses, And([ Not(r[0][j]) for j in range(1,k) ]))\n", + "\n", + " #3. Remaining elements $r_{i,0}$ in first column are true where x_i is true\n", + " clauses = And(clauses, And([Implies(x[i],r[i][0]) for i in range(1,n)]))\n", + "\n", + " #4. For rows 1:n-1, if the element above is true, this must be true\n", + "\n", + " for i in range(1,n):\n", + " for j in range(0,k):\n", + " clauses = And(clauses, Implies(r[i-1][j], r[i][j]))\n", + "\n", + " #5. If x is true for this row and the element above and to the left is true then set this element to true.\n", + " #6. If x is false for this row and the element above is false then set to false\n", + " #7. if x is false for this row and the element above and to the left is false then set to false:\n", + " for i in range(1,n):\n", + " for j in range(1,k):\n", + " clauses = And(clauses, Implies(And(x[i], r[i-1][j-1]), r[i][j]))\n", + " clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j])), Not(r[i][j])))\n", + " clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j-1])), Not(r[i][j])))\n", + "\n", + " #8. The bottom-right element of r must be true\n", + " clauses = And(clauses, r[n-1][k-1])\n", + "\n", + " return clauses" + ], + "metadata": { + "id": "aTcc1Ad0M9NX" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "#This function defined for convenience so that check_expression works\n", + "def at_least_three(x):\n", + " return at_least_k(x,3)\n", + "\n", + "check_expression(x, at_least_three, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, at_least_three, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, at_least_three, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, at_least_three, [True,True,True,True,True,True,True,True,True,True])" + ], + "metadata": { + "id": "ESnui2V7YBQC" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Optional: write functions to test if there are:\n", + "\n", + "* Fewer than $k$ elements\n", + "* Exactly $k$ elements\n", + "\n" + ], + "metadata": { + "id": "PwgpncA5g0-C" + } + }, + { + "cell_type": "code", + "source": [ + "def fewer_than_k(x, k):\n", + " # Create nxk table of literals r_{i,j}\n", + " n = len(x) ;\n", + " r = [[ z3.Bool(\"r_{%d,%d}\"%((i,j))) for j in range(0,k) ] for i in range(0,n) ]\n", + "\n", + " #1. Top left element $r_{0,0}$ is the first data element\n", + "\n", + " clauses = (r[0][0] == x[0])\n", + "\n", + " #2. Remaining elements $r_{0,1:}$ must be false\n", + "\n", + " clauses = And(clauses, And([ Not(r[0][j]) for j in range(1,k) ]))\n", + "\n", + " #3. Remaining elements $r_{i,0}$ in first column are true where x_i is true\n", + " clauses = And(clauses, And([Implies(x[i],r[i][0]) for i in range(1,n)]))\n", + "\n", + " #4. For rows 1:n-1, if the element above is true, this must be true\n", + " for i in range(1,n):\n", + " for j in range(0,k):\n", + " clauses = And(clauses, Implies(r[i-1][j], r[i][j]))\n", + "\n", + " #5. If x is true for this row and the element above and to the left is true then set this element to true.\n", + " #6. If x is false for this row and the element above is false then set to false\n", + " #7. if x is false for this row and the element above and to the left is false then set to false:\n", + " for i in range(1,n):\n", + " for j in range(1,k):\n", + " clauses = And(clauses, Implies(And(x[i], r[i-1][j-1]), r[i][j]))\n", + " clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j])), Not(r[i][j])))\n", + " clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j-1])), Not(r[i][j])))\n", + "\n", + " #8. The bottom-right element of r must be false\n", + " clauses = And(clauses, Not(r[n-1][k-1]))\n", + "\n", + " return clauses" + ], + "metadata": { + "id": "RS31wg5Ig0f-" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "#This function defined for convenience so that check_expression works\n", + "def fewer_than_three(x):\n", + " return fewer_than_k(x,3)\n", + "\n", + "check_expression(x, fewer_than_three, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, fewer_than_three, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, fewer_than_three, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, fewer_than_three, [True,True,True,True,True,True,True,True,True,True])" + ], + "metadata": { + "id": "Sy67NXs7hqDS" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "def exactly_k(x, k):\n", + " # Create nxk table of literals r_{i,j}\n", + " n = len(x) ;\n", + " r = [[ z3.Bool(\"r_{%d,%d}\"%((i,j))) for j in range(0,k+1) ] for i in range(0,n) ]\n", + "\n", + " #1. Top left element $r_{0,0}$ is the first data element\n", + "\n", + " clauses = (r[0][0] == x[0])\n", + "\n", + " #2. Remaining elements $r_{0,1:}$ must be false\n", + "\n", + " clauses = And(clauses, And([ Not(r[0][j]) for j in range(1,k+1) ]))\n", + "\n", + " #3. Remaining elements $r_{i,0}$ in first column are true where x_i is true\n", + " clauses = And(clauses, And([Implies(x[i],r[i][0]) for i in range(1,n)]))\n", + "\n", + " #4. For rows 1:n-1, if the element above is true, this must be true\n", + " for i in range(1,n):\n", + " for j in range(0,k+1):\n", + " clauses = And(clauses, Implies(r[i-1][j], r[i][j]))\n", + "\n", + " #5. If x is true for this row and the element above and to the left is true then set this element to true.\n", + " #6. If x is false for this row and the element above is false then set to false\n", + " #7. if x is false for this row and the element above and to the left is false then set to false:\n", + " for i in range(1,n):\n", + " for j in range(1,k+1):\n", + " clauses = And(clauses, Implies(And(x[i], r[i-1][j-1]), r[i][j]))\n", + " clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j])), Not(r[i][j])))\n", + " clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j-1])), Not(r[i][j])))\n", + "\n", + " #8. The bottom-right element of r must be\n", + " clauses = And(clauses, r[n-1][k-1])\n", + " clauses = And(clauses, Not(r[n-1][k]))\n", + "\n", + " return clauses" + ], + "metadata": { + "id": "Fzaa1NoaicKT" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "#This function defined for convenience so that check_expression works\n", + "def exactly_three(x):\n", + " return exactly_k(x,3)\n", + "\n", + "check_expression(x, exactly_three, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, exactly_three, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, exactly_three, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, exactly_three, [True,True,True,True,True,True,True,True,True,True])" + ], + "metadata": { + "id": "L_xwfybUkKhw" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "Now that we've finished, I'll let you into a secret. Z3 actually contains routines for (AtLeast, FewerThanOrEqualToo, and Exactly)" + ], + "metadata": { + "id": "H3lipx8akmHp" + } + }, + { + "cell_type": "code", + "source": [ + "def at_least_k_z3(x,k):\n", + " return PbGe([(i,1) for i in x],k)\n", + "\n", + "def at_least_three_z3(x):\n", + " return at_least_k_z3(x,3)\n", + "\n", + "check_expression(x, at_least_three_z3, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, at_least_three_z3, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, at_least_three_z3, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, at_least_three_z3, [True,True,True,True,True,True,True,True,True,True])" + ], + "metadata": { + "id": "Yho3WtG0luM6" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "def fewer_than_k_z3(x,k):\n", + " return PbLe([(i,1) for i in x],k-1)\n", + "\n", + "def fewer_than_three_z3(x):\n", + " return fewer_than_k_z3(x,3)\n", + "\n", + "check_expression(x, fewer_than_three_z3, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, fewer_than_three_z3, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, fewer_than_three_z3, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, fewer_than_three_z3, [True,True,True,True,True,True,True,True,True,True])" + ], + "metadata": { + "id": "ZjAMpiNFmJPc" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "def exactly_k_z3(x,k):\n", + " return PbEq([(i,1) for i in x],k)\n", + "\n", + "def exactly_three_z3(x):\n", + " return exactly_k_z3(x,3)\n", + "\n", + "check_expression(x, exactly_three_z3, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, exactly_three_z3, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, exactly_three_z3, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, exactly_three_z3, [True,True,True,True,True,True,True,True,True,True])" + ], + "metadata": { + "id": "EgG6jGAskUze" + }, + "execution_count": null, + "outputs": [] + } + ] +} \ No newline at end of file