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-12-03 11:05:25 -05:00
parent 75646c2c8e
commit c385687d8a
1 changed files with 12 additions and 28 deletions
Download Patch File Download Diff File Expand all files Collapse all files

40
Trees/SAT_Construction_Answers.ipynb
View File

@@ -4,7 +4,7 @@
"metadata": {
"colab": {
"provenance": [],
"authorship_tag": "ABX9TyNalp5KWVPvcXsJJ4jQvQ5U",
"authorship_tag": "ABX9TyMuosqLk/Qge3RUybmKsfO1",
"include_colab_link": true
},
"kernelspec": {
@@ -54,26 +54,9 @@
"cell_type": "code",
"execution_count": null,
"metadata": {
"id": "WZYb15hc19es",
"colab": {
"base_uri": "https://localhost:8080/"
},
"outputId": "d95ed66f-a8f7-422a-c6f4-1401d6bd06a5"
"id": "WZYb15hc19es"
},
"outputs": [
{
"output_type": "stream",
"name": "stdout",
"text": [
"Collecting z3-solver\n",
" Downloading z3_solver-4.14.1.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.metadata (602 bytes)\n",
"Downloading z3_solver-4.14.1.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (29.5 MB)\n",
"\u001b[2K \u001b[90m━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━\u001b[0m \u001b[32m29.5/29.5 MB\u001b[0m \u001b[31m20.4 MB/s\u001b[0m eta \u001b[36m0:00:00\u001b[0m\n",
"\u001b[?25hInstalling collected packages: z3-solver\n",
"Successfully installed z3-solver-4.14.1.0\n"
]
}
],
"outputs": [],
"source": [
"!pip install z3-solver\n",
"from z3 import *\n",
@@ -89,7 +72,7 @@
"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(\\lnot x_{1}\\land \\lnot x_{2}\\land \\lnot x_{3},\\ldots,\\lnot x_N).$$"
],
"metadata": {
"id": "aVj9RmuB3ZWJ"
@@ -282,7 +265,7 @@
"\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",
"$$ \\lnot 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",
@@ -298,11 +281,11 @@
"\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",
"$$ (\\lnot x_{i} \\land \\lnot r_{i-1,j}) \\Rightarrow \\lnot 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",
"7. if x is true 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",
"$$ (x_i \\land \\lnot{r}_{i-1,j-1})\\Rightarrow \\lnot{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",
@@ -344,7 +327,8 @@
" 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",
" clauses = And(clauses, Implies(And(x[i], Not(r[i-1][j-1])), Not(r[i][j])))\n",
"\n",
"\n",
" #8. The bottom-right element of r must be true\n",
" clauses = And(clauses, r[N-1][K-1])\n",
@@ -419,7 +403,7 @@
" 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",
" clauses = And(clauses, Implies(And(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",
@@ -481,7 +465,7 @@
" 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",
" clauses = And(clauses, Implies(And(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",