diff --git a/Trees/SAT_Construction_Answers.ipynb b/Trees/SAT_Construction_Answers.ipynb index 03de549..d503543 100644 --- a/Trees/SAT_Construction_Answers.ipynb +++ b/Trees/SAT_Construction_Answers.ipynb @@ -4,7 +4,7 @@ "metadata": { "colab": { "provenance": [], - "authorship_tag": "ABX9TyPyoipv7uhZXom6dIv+sZ0Z", + "authorship_tag": "ABX9TyOZqZK4GpOmpW/1ythp0bKH", "include_colab_link": true }, "kernelspec": { @@ -69,10 +69,10 @@ "source": [ "# Same\n", "\n", - "Let's write a subroutine that returns a Boolean logic formula that constrains $n$ variables to be the same.\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).$$" + "\\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" @@ -81,7 +81,7 @@ { "cell_type": "markdown", "source": [ - "First let's define the variables. We'll choose $n=10$" + "First let's define the variables. We'll choose $N=10$" ], "metadata": { "id": "Amv5G3VR3zIJ" @@ -90,8 +90,8 @@ { "cell_type": "code", "source": [ - "n=10\n", - "x = [ z3.Bool(\"x_{i}\".format(i=i)) for i in range(0,n) ]\n", + "N=10\n", + "x = [ z3.Bool(\"x_{i}\".format(i=i)) for i in range(0,N) ]\n", "print(x)" ], "metadata": { @@ -140,11 +140,7 @@ " # 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", + " s.add(And([x[i] if literal else Not(x[i]) for i, literal in enumerate(literals)]))\n", " # Check if it's SAT (creates the model)\n", " sat_result = s.check()\n", " if(sat_result==sat):\n", @@ -181,15 +177,15 @@ "\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", + "$$\\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", + "$$\\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", + "$$\\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:" ], @@ -217,6 +213,7 @@ " return Or(x)\n", "\n", "def no_more_than_one(x):\n", + " clauses = True ;\n", " for comb in combinations(x, 2):\n", " clauses = And([clauses, Or([Not(comb[0]), Not(comb[1])]) ])\n", " return clauses\n", @@ -242,10 +239,10 @@ { "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])" + "check_expression(x, exactly_one, [False,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, exactly_one, [True,False,False,False,False,False,False,False,False,False])\n", + "check_expression(x, exactly_one, [False,False,False,True,False,False,True,False,True,False])\n", + "check_expression(x, exactly_one, [True,True,True,True,True,True,True,True,True,True])" ], "metadata": { "id": "31gqasHnM3c3" @@ -258,9 +255,9 @@ "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", + "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", + "This one is a bit more complicated. We construct an NxK matrix of new literals $r_{i,j}$ Then we add the following constraints.\n", "\n", "1. Top left element $r_{0,0}$ is the first data element\n", "\n", @@ -268,31 +265,31 @@ "\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", + "$$ \\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", + "$$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", + "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", + "$$ 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", + "$$ (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", + "$$ (\\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", + "$$ (\\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}$$" + "$$ r_{N-1,K-1}$$" ], "metadata": { "id": "MJqWOMBsQrCI" @@ -301,10 +298,10 @@ { "cell_type": "code", "source": [ - "def at_least_k(x, k):\n", + "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 = 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", @@ -312,28 +309,28 @@ "\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", + " 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", + " 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", + " 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", + " 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", + " clauses = And(clauses, r[N-1][K-1])\n", "\n", " return clauses" ], @@ -366,8 +363,8 @@ "source": [ "Optional: write functions to test if there are:\n", "\n", - "* Fewer than $k$ elements\n", - "* Exactly $k$ elements\n", + "* Fewer than $K$ elements\n", + "* Exactly $N$ elements\n", "\n" ], "metadata": { @@ -377,10 +374,10 @@ { "cell_type": "code", "source": [ - "def fewer_than_k(x, k):\n", + "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 = 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", @@ -388,27 +385,27 @@ "\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", + " 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", + " 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", + " 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", + " 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", + " clauses = And(clauses, Not(r[N-1][K-1]))\n", "\n", " return clauses" ], @@ -439,10 +436,10 @@ { "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", + "def exactly_k(x, K):\n", + " # Create n x (k+1) 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", @@ -450,28 +447,28 @@ "\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", + " 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", + " 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", + " 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", + " 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", + " clauses = And(clauses, r[N-1][K-1])\n", + " clauses = And(clauses, Not(r[N-1][K]))\n", "\n", " return clauses" ], @@ -511,8 +508,8 @@ { "cell_type": "code", "source": [ - "def at_least_k_z3(x,k):\n", - " return PbGe([(i,1) for i in x],k)\n", + "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", @@ -531,8 +528,8 @@ { "cell_type": "code", "source": [ - "def fewer_than_k_z3(x,k):\n", - " return PbLe([(i,1) for i in x],k-1)\n", + "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", @@ -551,8 +548,8 @@ { "cell_type": "code", "source": [ - "def exactly_k_z3(x,k):\n", - " return PbEq([(i,1) for i in x],k)\n", + "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",