dr_domi/udlbook
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Created using Colab

Browse Source
This commit is contained in:
udlbook
2025-04-03 17:05:24 -04:00
parent eb29a28284
commit 1f0c224a7d
1 changed files with 65 additions and 68 deletions
Download Patch File Download Diff File Expand all files Collapse all files

133
Trees/SAT_Construction_Answers.ipynb
View File

@@ -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",