Add files via upload
This commit is contained in:
Peter Norvig authored and 
GitHub committed
1 parent
028aef4070
commit
8672ec00d9
1 file changed
+89
-54
+89
-54
@@ -15,12 +15,18 @@
|
|||||||
"|||\n",
|
"|||\n",
|
||||||
"\n",
|
"\n",
|
||||||
"\n",
|
"\n",
|
||||||
"In 2006, I wrote a [Python program](http://norvig.com/sudoku.html) to solve Sudoku. Soon after that, [Peter Seibel](https://gigamonkeys.com/) invited me to publish an article in [*Code Quarterly*](https://gigamonkeys.com/code-quarterly/) magazine which would go into more detail about backtracking search and constraint propagation in general, and would feature a more efficient program. Unfortunately, the magazine [folded](https://gigamonkeys.wordpress.com/2011/10/17/end-of-the-line-for-code-quarterly/) before I could finish the article. In 2021 I [updated the Python Sudoku program](Sudoku.ipynb) to Jupyter notebook form with modern coding idioms, and now I do the same for the [more efficient Java Sudoku program](Sudoku.java). \n",
|
"In 2006, I wrote a [Python program](http://norvig.com/sudoku.html) designed to solve any Sudoku puzzle. As computer security expert Ben Laurie has stated, Sudoku is \"a denial of service attack on human intellect\", and I thought maybe my program would convince people they didn't need to spend excessive time playing Sudoku. \n",
|
||||||
"\n",
|
"\n",
|
||||||
"I asked Claude and Codex to help me modernize my Java, and they were very good at that. I apologize if there are remaining legacy Java idioms from decades ago. The tools did not have any suggestions for how to make the code significantly faster (although the switch to a more modern threading API did make the code a few percent faster). I guess I did a good job of writing efficient Java way back in 2007.\n",
|
"In 2007, [Peter Seibel](https://gigamonkeys.com/) invited me to publish an article in [*Code Quarterly*](https://gigamonkeys.com/code-quarterly/) magazine which would go into more detail about backtracking search and constraint propagation in general, and would feature a more efficient program. Unfortunately, the magazine [folded](https://gigamonkeys.wordpress.com/2011/10/17/end-of-the-line-for-code-quarterly/) before I could finish [the article](https://www.norvig.com/CQ/sudoku.html). In 2021 I [updated the Python Sudoku program](Sudoku.ipynb) to Jupyter notebook form with modern coding idioms, and now I do the same for the [more efficient Java Sudoku program](Sudoku.java). \n",
|
||||||
|
"\n",
|
||||||
|
"I asked Claude and Codex to help me update my code from Java JDK 1.6 to Java JDK 26. They were very good at that. I also asked them for suggestions to make the code faster, but they didn't have any significant ideas (although the switch to a more modern threading API did speed throughput a few percent). I guess I did a good job of writing efficient Java way back in 2007.\n",
|
||||||
"\n",
|
"\n",
|
||||||
"- [**Sudoku.java**](Sudoku.java) is the Java program discussed in this notebook.\n",
|
"- [**Sudoku.java**](Sudoku.java) is the Java program discussed in this notebook.\n",
|
||||||
"- [**Sudoku.ipynb**](Sudoku.ipynb) is the original Python notebook."
|
"- [**Sudoku.ipynb**](Sudoku.ipynb) is the original Python notebook.\n",
|
||||||
|
"\n",
|
||||||
|
"<div class=\"alert alert-block alert-success\">\n",
|
||||||
|
"<b><i>TLDR: The program solves over 400,000 puzzles per second , and over 30,000 puzzles per second on the hardest puzzles.</b> <i>\n",
|
||||||
|
"</div>"
|
||||||
]
|
]
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
@@ -29,7 +35,7 @@
|
|||||||
"source": [
|
"source": [
|
||||||
"# Solving a Puzzle\n",
|
"# Solving a Puzzle\n",
|
||||||
"\n",
|
"\n",
|
||||||
"In the file [sudokus1.txt](sudokus1.txt) is the single puzzle shown at the top of the page, in this format (one puzzle per line):"
|
"In the file [sudokus1.txt](sudokus1.txt) is the single puzzle shown at the top of the page, in this format:"
|
||||||
]
|
]
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
@@ -164,7 +170,7 @@
|
|||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"source": [
|
"source": [
|
||||||
"Let's run the `java Sudoku` program on all these puzzles, and show the timing results. To get even more puzzles (more puzzles should lower timing variance), I use the `-r` option to include the reverse of each puzzle (the last square becomes the first, etc.) and `-R` to repeat puzzles."
|
"Let's run the `java Sudoku` program on all these puzzles, and show the timing results. To get even more puzzles (to lower timing variance), I use the `-r` option to include the reverse of each puzzle (the last square becomes the first, etc.) and `-R` to repeat puzzles."
|
||||||
]
|
]
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
@@ -178,9 +184,9 @@
|
|||||||
"text": [
|
"text": [
|
||||||
"Puzzles μsec KHz Threads Backtracks Name\n",
|
"Puzzles μsec KHz Threads Backtracks Name\n",
|
||||||
"======= ====== ======= ======= ========== ====\n",
|
"======= ====== ======= ======= ========== ====\n",
|
||||||
" 30000 27.5 36.392 28 330.7 sudokus_hard.txt\n",
|
" 30000 29.1 34.403 28 330.7 sudokus_hard.txt\n",
|
||||||
" 983020 2.0 500.670 28 41.7 sudokus_17.txt\n",
|
" 983020 2.0 497.578 28 41.7 sudokus_17.txt\n",
|
||||||
"1000000 2.5 400.960 28 32.5 sudokus.txt\n"
|
"1000000 2.5 402.050 28 32.5 sudokus.txt\n"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
@@ -192,11 +198,7 @@
|
|||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"source": [
|
"source": [
|
||||||
"**Conclusion: The program solves about 35,000 puzzles per second with the hardest puzzles, and about 400,000 per second (or more) with easier puzzles.** \n",
|
"So the program is solving 34,000 puzzles per second on the hardest puzzles, and about 400,000 to 500,000 on the other files of more average-difficulty puzzles. The columns of the output are:\n",
|
||||||
"\n",
|
|
||||||
"This is a pretty good performance for such a simple program! One of the fastest known Sudoku solvers, [**tdoku**](https://github.com/t-dillon/tdoku), reports similar speed (but that was in 2020, so they probably used a slower computer than my 28-core 96 GB Mac Studio M3 Ultra).\n",
|
|
||||||
"\n",
|
|
||||||
"The columns of the output are:\n",
|
|
||||||
"\n",
|
"\n",
|
||||||
"- `Puzzles`: the total number of puzzles solved.\n",
|
"- `Puzzles`: the total number of puzzles solved.\n",
|
||||||
"- `μsec`: the mean time to solve a puzzle in microseconds (millionths of a second).\n",
|
"- `μsec`: the mean time to solve a puzzle in microseconds (millionths of a second).\n",
|
||||||
@@ -205,8 +207,11 @@
|
|||||||
"- `Backtracks`: the average number of times per puzzle that the search guessed wrong and had to back up.\n",
|
"- `Backtracks`: the average number of times per puzzle that the search guessed wrong and had to back up.\n",
|
||||||
"- `Name`: here the name of the file; could also be a puzzle number when -p option is on.\n",
|
"- `Name`: here the name of the file; could also be a puzzle number when -p option is on.\n",
|
||||||
"\n",
|
"\n",
|
||||||
|
"One of the fastest known Sudoku solvers, [**tdoku**](https://github.com/t-dillon/tdoku), reports similar speed (but that was in 2020, so they probably used a slower computer than my 28-core 96 GB Mac Studio M3 Ultra).\n",
|
||||||
"\n",
|
"\n",
|
||||||
"Note that the μsec and KHz columns are displaying **throughput**: the number of puzzles that can be solved in a given amount of time. This is different than **latency**: the time it takes to solve a single puzzle from start to end. Throughput and latency are different because there are multiple threads working in parallel. If, say, there are 25 threads working in parallel on 25 CPUs and each puzzle takes 1 second to solve, then latency would be 1 second but throughput would be 25 puzzles per second. I did some experiments, and on my machine (an M3 Ultra Mac Studio), the best performance is somewhere around 25 threads (although there is 5% to 10% variance from run to run, so I couldn't nail down an optimal number). \n",
|
"# Throughput versus Latency\n",
|
||||||
|
"\n",
|
||||||
|
"Note that the μsec and KHz columns are displaying **throughput**: the number of puzzles that can be solved in a given amount of time. This is different than **latency**: the time it takes to solve a single puzzle from start to end. Throughput and latency are different because there are multiple threads working in parallel. If, say, there are 28 threads working in parallel on 28 CPUs and each puzzle takes 1 second to solve, then latency would be 1 second but throughput would be 28 puzzles per second. \n",
|
||||||
"\n",
|
"\n",
|
||||||
"To measure the latency, use the `-T1` option to request a single thread:"
|
"To measure the latency, use the `-T1` option to request a single thread:"
|
||||||
]
|
]
|
||||||
@@ -222,9 +227,9 @@
|
|||||||
"text": [
|
"text": [
|
||||||
"Puzzles μsec KHz Threads Backtracks Name\n",
|
"Puzzles μsec KHz Threads Backtracks Name\n",
|
||||||
"======= ====== ======= ======= ========== ====\n",
|
"======= ====== ======= ======= ========== ====\n",
|
||||||
" 3000 286.2 3.495 1 292.2 sudokus_hard.txt\n",
|
" 3000 281.9 3.547 1 292.2 sudokus_hard.txt\n",
|
||||||
" 49151 70.7 14.138 1 40.2 sudokus_17.txt\n",
|
" 49151 69.3 14.430 1 40.2 sudokus_17.txt\n",
|
||||||
" 250000 67.0 14.932 1 34.2 sudokus.txt\n"
|
" 250000 66.3 15.082 1 34.2 sudokus.txt\n"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
@@ -259,8 +264,8 @@
|
|||||||
"text": [
|
"text": [
|
||||||
"Puzzles μsec KHz Threads Backtracks Name\n",
|
"Puzzles μsec KHz Threads Backtracks Name\n",
|
||||||
"======= ====== ======= ======= ========== ====\n",
|
"======= ====== ======= ======= ========== ====\n",
|
||||||
"1000000 2.6 378.661 28 32.5 sudokus.txt\n",
|
"1000000 2.5 395.567 28 32.5 sudokus.txt\n",
|
||||||
"1000000 4.2 240.693 28 107.4 sudokus.txt\n"
|
"1000000 4.2 237.418 28 107.4 sudokus.txt\n"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
@@ -336,50 +341,74 @@
|
|||||||
" <tbody>\n",
|
" <tbody>\n",
|
||||||
" <tr>\n",
|
" <tr>\n",
|
||||||
" <th>count</th>\n",
|
" <th>count</th>\n",
|
||||||
" <td>49528.000000</td>\n",
|
" <td>49527.000000</td>\n",
|
||||||
" <td>49528.000000</td>\n",
|
" <td>49527.000000</td>\n",
|
||||||
" <td>49528.000000</td>\n",
|
" <td>49527.000000</td>\n",
|
||||||
" </tr>\n",
|
" </tr>\n",
|
||||||
" <tr>\n",
|
" <tr>\n",
|
||||||
" <th>mean</th>\n",
|
" <th>mean</th>\n",
|
||||||
" <td>74.375662</td>\n",
|
" <td>74.695403</td>\n",
|
||||||
" <td>23.166825</td>\n",
|
" <td>23.262107</td>\n",
|
||||||
" <td>42.145663</td>\n",
|
" <td>42.144939</td>\n",
|
||||||
" </tr>\n",
|
" </tr>\n",
|
||||||
" <tr>\n",
|
" <tr>\n",
|
||||||
" <th>std</th>\n",
|
" <th>std</th>\n",
|
||||||
" <td>151.413051</td>\n",
|
" <td>152.543361</td>\n",
|
||||||
" <td>11.061670</td>\n",
|
" <td>11.191693</td>\n",
|
||||||
" <td>187.343129</td>\n",
|
" <td>187.344951</td>\n",
|
||||||
" </tr>\n",
|
" </tr>\n",
|
||||||
" <tr>\n",
|
" <tr>\n",
|
||||||
" <th>min</th>\n",
|
" <th>min</th>\n",
|
||||||
" <td>11.800000</td>\n",
|
" <td>12.000000</td>\n",
|
||||||
" <td>0.102000</td>\n",
|
" <td>0.099000</td>\n",
|
||||||
|
" <td>0.000000</td>\n",
|
||||||
|
" </tr>\n",
|
||||||
|
" <tr>\n",
|
||||||
|
" <th>1%</th>\n",
|
||||||
|
" <td>18.300000</td>\n",
|
||||||
|
" <td>1.663300</td>\n",
|
||||||
|
" <td>0.000000</td>\n",
|
||||||
|
" </tr>\n",
|
||||||
|
" <tr>\n",
|
||||||
|
" <th>10%</th>\n",
|
||||||
|
" <td>27.800000</td>\n",
|
||||||
|
" <td>8.029000</td>\n",
|
||||||
" <td>0.000000</td>\n",
|
" <td>0.000000</td>\n",
|
||||||
" </tr>\n",
|
" </tr>\n",
|
||||||
" <tr>\n",
|
" <tr>\n",
|
||||||
" <th>25%</th>\n",
|
" <th>25%</th>\n",
|
||||||
" <td>33.000000</td>\n",
|
" <td>32.800000</td>\n",
|
||||||
" <td>15.405000</td>\n",
|
" <td>15.414000</td>\n",
|
||||||
" <td>1.000000</td>\n",
|
" <td>1.000000</td>\n",
|
||||||
" </tr>\n",
|
" </tr>\n",
|
||||||
" <tr>\n",
|
" <tr>\n",
|
||||||
" <th>50%</th>\n",
|
" <th>50%</th>\n",
|
||||||
" <td>42.500000</td>\n",
|
" <td>42.400000</td>\n",
|
||||||
" <td>23.553000</td>\n",
|
" <td>23.599000</td>\n",
|
||||||
" <td>5.000000</td>\n",
|
" <td>5.000000</td>\n",
|
||||||
" </tr>\n",
|
" </tr>\n",
|
||||||
" <tr>\n",
|
" <tr>\n",
|
||||||
" <th>75%</th>\n",
|
" <th>75%</th>\n",
|
||||||
" <td>64.900000</td>\n",
|
" <td>64.900000</td>\n",
|
||||||
" <td>30.303000</td>\n",
|
" <td>30.534000</td>\n",
|
||||||
" <td>24.000000</td>\n",
|
" <td>24.000000</td>\n",
|
||||||
" </tr>\n",
|
" </tr>\n",
|
||||||
" <tr>\n",
|
" <tr>\n",
|
||||||
|
" <th>90%</th>\n",
|
||||||
|
" <td>124.500000</td>\n",
|
||||||
|
" <td>36.036000</td>\n",
|
||||||
|
" <td>80.000000</td>\n",
|
||||||
|
" </tr>\n",
|
||||||
|
" <tr>\n",
|
||||||
|
" <th>99%</th>\n",
|
||||||
|
" <td>601.058000</td>\n",
|
||||||
|
" <td>54.546000</td>\n",
|
||||||
|
" <td>646.740000</td>\n",
|
||||||
|
" </tr>\n",
|
||||||
|
" <tr>\n",
|
||||||
" <th>max</th>\n",
|
" <th>max</th>\n",
|
||||||
" <td>9770.700000</td>\n",
|
" <td>10108.800000</td>\n",
|
||||||
" <td>85.106000</td>\n",
|
" <td>83.626000</td>\n",
|
||||||
" <td>13438.000000</td>\n",
|
" <td>13438.000000</td>\n",
|
||||||
" </tr>\n",
|
" </tr>\n",
|
||||||
" </tbody>\n",
|
" </tbody>\n",
|
||||||
@@ -388,14 +417,18 @@
|
|||||||
],
|
],
|
||||||
"text/plain": [
|
"text/plain": [
|
||||||
" μsec KHz Backtracks\n",
|
" μsec KHz Backtracks\n",
|
||||||
"count 49528.000000 49528.000000 49528.000000\n",
|
"count 49527.000000 49527.000000 49527.000000\n",
|
||||||
"mean 74.375662 23.166825 42.145663\n",
|
"mean 74.695403 23.262107 42.144939\n",
|
||||||
"std 151.413051 11.061670 187.343129\n",
|
"std 152.543361 11.191693 187.344951\n",
|
||||||
"min 11.800000 0.102000 0.000000\n",
|
"min 12.000000 0.099000 0.000000\n",
|
||||||
"25% 33.000000 15.405000 1.000000\n",
|
"1% 18.300000 1.663300 0.000000\n",
|
||||||
"50% 42.500000 23.553000 5.000000\n",
|
"10% 27.800000 8.029000 0.000000\n",
|
||||||
"75% 64.900000 30.303000 24.000000\n",
|
"25% 32.800000 15.414000 1.000000\n",
|
||||||
"max 9770.700000 85.106000 13438.000000"
|
"50% 42.400000 23.599000 5.000000\n",
|
||||||
|
"75% 64.900000 30.534000 24.000000\n",
|
||||||
|
"90% 124.500000 36.036000 80.000000\n",
|
||||||
|
"99% 601.058000 54.546000 646.740000\n",
|
||||||
|
"max 10108.800000 83.626000 13438.000000"
|
||||||
]
|
]
|
||||||
},
|
},
|
||||||
"execution_count": 9,
|
"execution_count": 9,
|
||||||
@@ -407,15 +440,16 @@
|
|||||||
"import pandas as pd\n",
|
"import pandas as pd\n",
|
||||||
"\n",
|
"\n",
|
||||||
"columns = 'Puzzles μsec KHz Threads Backtracks Puzzle Number'.split()\n",
|
"columns = 'Puzzles μsec KHz Threads Backtracks Puzzle Number'.split()\n",
|
||||||
"sudata = pd.read_csv('sudata.txt', sep='\\s+', names=columns).drop(columns=['Puzzles', 'Puzzle', 'Threads', 'Number'])\n",
|
"sudata = pd.read_csv('sudata.txt', sep='\\s+', usecols=(1, 2, 4))\n",
|
||||||
"sudata.describe()"
|
"sudata.columns = ('μsec', 'KHz', 'Backtracks')\n",
|
||||||
|
"sudata.describe(percentiles=(.01, .10, .25, .50, .75, .90, .99))"
|
||||||
]
|
]
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"source": [
|
"source": [
|
||||||
"The mean latency is 74 microseconds, the median is about 42 microseconds, and the maximum is about 10 milliseconds. For number of backtracks, the mean is 42, the median is only 5, and the maximum is over 13,000. \n",
|
"The mean latency is 74 microseconds, the median is about 42 microseconds, and the maximum is about 10 milliseconds. For number of backtracks, the mean is 42, the median is only 5, at least 25% have zero or one backtrack, and the maximum is over 13,000. \n",
|
||||||
"\n",
|
"\n",
|
||||||
"Here is a scatterplot:"
|
"Here is a scatterplot:"
|
||||||
]
|
]
|
||||||
@@ -427,7 +461,7 @@
|
|||||||
"outputs": [
|
"outputs": [
|
||||||
{
|
{
|
||||||
"data": {
|
"data": {
|
||||||
"image/png": "iVBORw0KGgoAAAANSUhEUgAAAmAAAAGwCAYAAAAOvdliAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjYsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvq6yFwwAAAAlwSFlzAAAPYQAAD2EBqD+naQAARQdJREFUeJzt3Xt8VNXd7/HvJCFDiMlAgskQuQWICg1eCBBAHwGJQMulrW3RgvFSi/jILd5Aj/VobQX1sQIKKlof7VFbqlV67COlBEQECYETTAURuQUIlxguYQIScpt1/oBsM7lACGHPJPN5v155vZg9a/Zee9Vmvln7t9d2GGOMAAAAYJsQf3cAAAAg2BDAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALBZmL870JJ4vV4dOHBAUVFRcjgc/u4OAABoAGOMjh8/roSEBIWE2DM3RQBrQgcOHFCnTp383Q0AANAI+fn56tixoy3HIoA1oaioKEmn/weMjo72c28AAEBDFBcXq1OnTtb3uB0IYE2o6rJjdHQ0AQwAgGbGzvIhivABAABsRgADAACwmV8D2GeffaYxY8YoISFBDodDf//7333eN8boySefVEJCgiIiIjRkyBB99dVXPm1KS0s1depUtW/fXpGRkRo7dqz27dvn06aoqEjp6elyuVxyuVxKT0/XsWPHfNrs3btXY8aMUWRkpNq3b69p06aprKzsYpw2AAAIcn4NYN99952uvvpqzZ8/v873n3vuOb3wwguaP3++NmzYILfbrZtuuknHjx+32mRkZGjx4sVatGiR1qxZoxMnTmj06NGqrKy02owfP165ublaunSpli5dqtzcXKWnp1vvV1ZWatSoUfruu++0Zs0aLVq0SB988IEefPDBi3fyAAAgeJkAIcksXrzYeu31eo3b7TbPPPOMte3UqVPG5XKZV1991RhjzLFjx0yrVq3MokWLrDb79+83ISEhZunSpcYYY7Zs2WIkmXXr1lltsrKyjCSzdetWY4wxS5YsMSEhIWb//v1Wm7/85S/G6XQaj8fT4HPweDxG0nl9BgAA+Jc/vr8DtgYsLy9PBQUFGj58uLXN6XRq8ODBWrt2rSQpJydH5eXlPm0SEhKUnJxstcnKypLL5VJqaqrVZsCAAXK5XD5tkpOTlZCQYLUZMWKESktLlZOTU28fS0tLVVxc7PMDAABwLgEbwAoKCiRJ8fHxPtvj4+Ot9woKChQeHq527dqdtU1cXFyt/cfFxfm0qXmcdu3aKTw83GpTl9mzZ1t1ZS6Xi0VYAQBAgwRsAKtSc00OY8w51+mo2aau9o1pU9Ojjz4qj8dj/eTn55+1XwAAAFIABzC32y1JtWagCgsLrdkqt9utsrIyFRUVnbXNt99+W2v/hw4d8mlT8zhFRUUqLy+vNTNWndPptBZdZfFVAADQUAEbwBITE+V2u5WZmWltKysr06pVqzRo0CBJUkpKilq1auXT5uDBg9q8ebPVZuDAgfJ4PFq/fr3VJjs7Wx6Px6fN5s2bdfDgQavNsmXL5HQ6lZKSclHPEwAABB+/PoroxIkT2rFjh/U6Ly9Pubm5iomJUefOnZWRkaFZs2YpKSlJSUlJmjVrltq0aaPx48dLklwul+6++249+OCDio2NVUxMjB566CH17t1baWlpkqSePXtq5MiRmjhxohYuXChJuueeezR69GhdccUVkqThw4erV69eSk9P13/913/p6NGjeuihhzRx4kRmtQAAQNOz7X7LOqxcudJIqvVzxx13GGNOL0XxxBNPGLfbbZxOp7nhhhvMpk2bfPZRUlJipkyZYmJiYkxERIQZPXq02bt3r0+bI0eOmAkTJpioqCgTFRVlJkyYYIqKinza7Nmzx4waNcpERESYmJgYM2XKFHPq1KnzOh+WoQAAoPnxx/e3wxhj/Jj/WpTi4mK5XC55PB5mzgAAaCIVlV4tWLlTG3YfVb+uMZo8tLvCQpuuisof399+vQQJAABwLgtW7tTc5dtkJH2+47AkaXpakn87dYECtggfAABAkjbsPqqqy3XmzOvmjgAGAAACWr+uMapaldNx5nVzxyVIAAAQ0CYP7S5JPjVgzR0BDAAABLSw0JBmX/NVE5cgAQAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGwW0AGsoqJCv/nNb5SYmKiIiAh169ZNTz31lLxer9XGGKMnn3xSCQkJioiI0JAhQ/TVV1/57Ke0tFRTp05V+/btFRkZqbFjx2rfvn0+bYqKipSeni6XyyWXy6X09HQdO3bMjtMEAABBJqAD2LPPPqtXX31V8+fP19dff63nnntO//Vf/6WXXnrJavPcc8/phRde0Pz587Vhwwa53W7ddNNNOn78uNUmIyNDixcv1qJFi7RmzRqdOHFCo0ePVmVlpdVm/Pjxys3N1dKlS7V06VLl5uYqPT3d1vMFAADBwWGMMf7uRH1Gjx6t+Ph4vfHGG9a2n/3sZ2rTpo3efvttGWOUkJCgjIwMzZw5U9Lp2a74+Hg9++yzmjRpkjwejy699FK9/fbbuuWWWyRJBw4cUKdOnbRkyRKNGDFCX3/9tXr16qV169YpNTVVkrRu3ToNHDhQW7du1RVXXNGg/hYXF8vlcsnj8Sg6OrqJRwMAAFwM/vj+DugZsOuvv14rVqzQtm3bJEn//ve/tWbNGv3oRz+SJOXl5amgoEDDhw+3PuN0OjV48GCtXbtWkpSTk6Py8nKfNgkJCUpOTrbaZGVlyeVyWeFLkgYMGCCXy2W1qUtpaamKi4t9fgAAAM4lzN8dOJuZM2fK4/HoyiuvVGhoqCorK/X000/rl7/8pSSpoKBAkhQfH+/zufj4eO3Zs8dqEx4ernbt2tVqU/X5goICxcXF1Tp+XFyc1aYus2fP1m9/+9vGnyAAAAhKAT0D9te//lXvvPOO/vznP2vjxo3605/+pOeff15/+tOffNo5HA6f18aYWttqqtmmrvbn2s+jjz4qj8dj/eTn5zfktAAAQJAL6Bmwhx9+WI888ohuvfVWSVLv3r21Z88ezZ49W3fccYfcbrek0zNYHTp0sD5XWFhozYq53W6VlZWpqKjIZxassLBQgwYNstp8++23tY5/6NChWrNr1TmdTjmdzgs/UQAAEFQCegbs5MmTCgnx7WJoaKi1DEViYqLcbrcyMzOt98vKyrRq1SorXKWkpKhVq1Y+bQ4ePKjNmzdbbQYOHCiPx6P169dbbbKzs+XxeKw2AAAATSWgZ8DGjBmjp59+Wp07d9YPfvADffHFF3rhhRf0q1/9StLpy4YZGRmaNWuWkpKSlJSUpFmzZqlNmzYaP368JMnlcunuu+/Wgw8+qNjYWMXExOihhx5S7969lZaWJknq2bOnRo4cqYkTJ2rhwoWSpHvuuUejR49u8B2QAAAADRXQAeyll17S448/rvvuu0+FhYVKSEjQpEmT9L//9/+22syYMUMlJSW67777VFRUpNTUVC1btkxRUVFWmzlz5igsLEzjxo1TSUmJhg0bprfeekuhoaFWm3fffVfTpk2z7pYcO3as5s+fb9/JAgCAoBHQ64A1N6wDBgBA88M6YAAAAEGAAAYAAGAzAhgAAIDNCGAAAAA2I4ABAADYjAAGAABgMwIYAACAzQhgAAAANiOAAQAA2IwABgAAYDMCGAAAgM0IYAAAADYjgAEAANiMAAYAAGAzAhgAAIDNCGAAAAA2I4ABAADYjAAGAABgMwIYAACAzQhgAAAANiOAAQAA2IwABgAAYDMCGAAAgM0IYAAAADYjgAEAANiMAAYAAGAzAhgAAIDNCGAAAAA2I4ABAADYjAAGAABgMwIYAACAzQhgAAAANiOAAQAA2IwABgAAYDMCGAAAgM0IYAAAADYjgAEAANiMAAYAAGAzAhgAAIDNwvzdAQDAxVdR6dWClTu1YfdR9esao8lDuysslL/BAX8hgAFAEFiwcqfmLt8mI+nzHYclSdPTkvzbKSCI8ecPAASBDbuPypz5tznzGoD/EMAAIAj06xojx5l/O868BuA/XIIEgCAweWh3SfKpAQPgPwQwAAgCYaEh1HwBAYRLkAAAADYjgAEAANiMAAYAAGAzAhgAAIDNCGAAAAA2I4ABAADYjAAGAABgMwIYAACAzQhgAAAANiOAAQAA2IwABgAAYDMCGAAAgM0IYAAAADYL+AC2f/9+3XbbbYqNjVWbNm10zTXXKCcnx3rfGKMnn3xSCQkJioiI0JAhQ/TVV1/57KO0tFRTp05V+/btFRkZqbFjx2rfvn0+bYqKipSeni6XyyWXy6X09HQdO3bMjlMEAABBJqADWFFRka677jq1atVK//znP7Vlyxb94Q9/UNu2ba02zz33nF544QXNnz9fGzZskNvt1k033aTjx49bbTIyMrR48WItWrRIa9as0YkTJzR69GhVVlZabcaPH6/c3FwtXbpUS5cuVW5urtLT0+08XQAAECQcxhjj707U55FHHtHnn3+u1atX1/m+MUYJCQnKyMjQzJkzJZ2e7YqPj9ezzz6rSZMmyePx6NJLL9Xbb7+tW265RZJ04MABderLine truncated
|
"image/png": "iVBORw0KGgoAAAANSUhEUgAAAmAAAAGwCAYAAAAOvdliAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjYsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvq6yFwwAAAAlwSFlzAAAPYQAAD2EBqD+naQAARG9JREFUeJzt3Xl8VNX9//H3JIEhYBhIkISwBokKDSqEXSsgEbAsbW2LFoxiLdoqSxQE/FJ/Lq0g1AooLmB9SL9qS7VKv1opEhARJAQaSAUR2QIJS0QgTEBCtjm/PyDXTDZCSO5MMq/n45HHN3PnzL3n3vpl3jnnc891GGOMAAAAYJsgX3cAAAAg0BDAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALBZiK870JB4PB4dOXJEYWFhcjgcvu4OAACoBmOMTp8+rejoaAUF2TM2RQCrRUeOHFH79u193Q0AAFADWVlZateunS3HIoDVorCwMEnn/wds3ry5j3sDAACqIzc3V+3bt7e+x+1AAKtFJdOOzZs3J4ABAFDP2Fk+RBE+AACAzQhgAAAANiOAAQAA2IwABgAAYDMCGAAAgM0IYAAAADYjgAEAANiMAAYAAGAzAhgAAIDNCGAAAAA2I4ABAADYjAAGAABgMx7GDQAA/FpRsUcvrd2nLQdOqnencD00+CqFBNfvMSQCGAAA8Gsvrd2nBat3y0j6fO9xSdKUhFjfduoy+TQ+fvbZZxo1apSio6PlcDj0z3/+0+t9Y4yefPJJRUdHKzQ0VIMGDdKXX37p1SY/P1+TJk1Sq1at1KxZM40ePVqHDh3yapOTk6PExES5XC65XC4lJibq1KlTXm0yMzM1atQoNWvWTK1atdLkyZNVUFBQF6cNAAAuwZYDJ2Uu/G4uvK7vfBrAvvvuO11//fVatGhRhe/PmzdPzz//vBYtWqQtW7YoKipKt956q06fPm21SUpK0vLly7Vs2TJt2LBBZ86c0ciRI1VcXGy1GTt2rNLT07Vy5UqtXLlS6enpSkxMtN4vLi7WiBEj9N1332nDhg1atmyZ3nvvPU2dOrXuTh4AAFRL707hclz43XHhdb1n/IQks3z5cuu1x+MxUVFR5tlnn7W2nTt3zrhcLvPqq68aY4w5deqUadSokVm2bJnV5vDhwyYoKMisXLnSGGPMzp07jSSzadMmq01KSoqRZHbt2mWMMWbFihUmKCjIHD582Grzt7/9zTidTuN2u6t9Dm6320i6pM8AAICqFRYVmwXJu8241zaZBcm7TWFRca3u3xff335bwZaRkaHs7GwNHTrU2uZ0OjVw4EBt3LhRkpSWlqbCwkKvNtHR0YqLi7PapKSkyOVyqW/fvlabfv36yeVyebWJi4tTdHS01WbYsGHKz89XWlpapX3Mz89Xbm6u1w8AAKhdIcFBmpIQq7d+3VdTEmLrfQG+5MfLUGRnZ0uSIiMjvbZHRkZa72VnZ6tx48Zq2bJllW1at25dbv+tW7f2alP2OC1btlTjxo2tNhWZM2eOVVfmcrnUvn37SzxLAAAQiPw2gJVwOBxer40x5baVVbZNRe1r0qasxx57TG632/rJysqqsl8AAACSHwewqKgoSSo3AnXs2DFrtCoqKkoFBQXKycmpss0333xTbv/ffvutV5uyx8nJyVFhYWG5kbHSnE6nmjdv7vUDAABwMX4bwGJiYhQVFaXk5GRrW0FBgdatW6cBAwZIkuLj49WoUSOvNkePHtWOHTusNv3795fb7dbmzZutNqmpqXK73V5tduzYoaNHj1ptVq1aJafTqfj4+Do9TwAAEHh8uhDrmTNntHfvXut1RkaG0tPTFR4erg4dOigpKUmzZ89WbGysYmNjNXv2bDVt2lRjx46VJLlcLt13332aOnWqIiIiFB4ermnTpql79+5KSEiQJHXt2lXDhw/XhAkTtHjxYknS/fffr5EjR+qaa66RJA0dOlTdunVTYmKi/vjHP+rkyZOaNm2aJkyYwKgWAACofbbdb1mBtWvXGp1fU83r55577jHGnF+K4oknnjBRUVHG6XSam2++2Wzfvt1rH3l5eWbixIkmPDzchIaGmpEjR5rMzEyvNidOnDDjxo0zYWFhJiwszIwbN87k5OR4tTl48KAZMWKECQ0NNeHh4WbixInm3Llzl3Q+LEMBAED944vvb4cxxlSRz3AJcnNz5XK55Ha7GTkDAKCe8MX3t9/WgAEAADRUBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbObXAayoqEi/+93vFBMTo9DQUHXu3FlPP/20PB6P1cYYoyeffFLR0dEKDQ3VoEGD9OWXX3rtJz8/X5MmTVKrVq3UrFkzjR49WocOHfJqk5OTo8TERLlcLrlcLiUmJurUqVN2nCYAAAgwfh3A5s6dq1dffVWLFi3SV199pXnz5umPf/yjXnzxRavNvHnz9Pzzz2vRokXasmWLoqKidOutt+r06dNWm6SkJC1fvlzLli3Thg0bdObMGY0cOVLFxcVWm7Fjxyo9PV0rV67UypUrlZ6ersTERFvPFwAABAaHMcb4uhOVGTlypCIjI/X6669b2372s5+padOmevPNN2WMUXR0tJKSkjRjxgxJ50e7IiMjNXfuXD3wwANyu9268sor9eabb+qOO+6QJB05ckTt27fXihUrNGzYMH311Vfq1q2bNm3apL59+0qSNm3apP79+2vXrl265pprqtXf3NxcuVwuud1uNW/evJavBgAAqAu++P726xGwm266SWvWrNHu3bslSf/973+1YcMG/ehHP5IkZWRkKDs7W0OHDrU+43Q6NXDgQG3cuFGSlJaWpsLCQq820dHRiouLs9qkpKTI5XJZ4UuS+vXrJ5fLZbWpSH5+vnJzc71+AAAALibE1x2oyowZM+R2u3XttdcqODhYxcXFeuaZZ/TLX/5SkpSdnS1JioyM9PpcZGSkDh48aLVp3LixWrZsWa5Nyeezs7PVunXrcsdv3bq11aYic+bM0VNPPVXzEwQAAAHJr0fA/v73v+utt97SX//6V23dulV/+ctf9Nxzz+kvf/mLVzuHw+H12hhTbltZZdtU1P5i+3nsscfkdrutn6ysrOqcFgAACHB+PQL26KOPaubMmbrzzjslSd27d9fBgwc1Z84c3XPPPYqKipJ0fgSrTZs21ueOHTtmjYpFRUWpoKBAOTk5XqNgx44d04ABA6w233zzTbnjf/vtt+VG10pzOp1yOp2Xf6IAACCg+PUI2NmzZxUU5N3F4OBgaxmKmJgYRUVFKTk52Xq/oKBA69ats8JVfHy8GjVq5NXm6NGj2rFjh9Wmf//+crvd2rx5s9UmNTVVbrfbagMAAFBb/HoEbNSoUXrmmWfUoUMH/eAHP9C2bdv0/PPP61e/+pWk89OGSUlJmj17tmJjYxUbG6vZs2eradOmGjt2rCTJ5XLpvvvu09SpUxUREaHw8HBNmzZN3bt3V0JCgiSpa9euGj58uCZMmKDFixdLku6//36NHDmy2ndAAgAAVJdfB7AXX3xRjz/+uB588EEdO3ZM0dHReuCBB/T//t//s9pMnz5deXl5evDBB5WTk6O+fftq1apVCgsLs9rMnz9fISEhGjNmjPLy8jRkyBAtXbpUwcHBVpu3335bkydPtu6WHD16tBYtWmTfyQIAgIDh1+uA1TesAwYAQP3DOmAAAAABgAAGAABgMwIYAACAzQhgAAAANiOAAQAA2IwABgAAYDMCGAAAgM0IYAAAADYjgAEAANiMAAYAAGAzAhgAAIDNCGAAAAA2I4ABAADYjAAGAABgMwIYAACAzQhgAAAANiOAAQAA2IwABgAAYDMCGAAAgM0IYAAAADYjgAEAANiMAAYAAGAzAhgAAIDNCGAAAAA2I4ABAADYjAAGAABgMwIYAACAzQhgAAAANiOAAQAA2CzE1x0AANS9omKPXlq7T1sOnFTvTuF6aPBVCgnmb3DAVwhgABAAXlq7TwtW75aR9Pne45KkKQmxvu0UEMD48wcAAsCWAydlLvxuLrwG4DsEMAAIAL07hctx4XfHhdcAfIcpSAAIAA8NvkqSvGrAAPgOAQwAAkBIcBA1X4AfYQoSAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmBDAAAACbEcAAAABsRgADAACwGQEMAADAZgQwAAAAmxHAAAAAbEYAAwAAsBkBDAAAwGYEMAAAAJsRwAAAAGxGAAMAALAZAQwAAMBmfh/ADh8+rLvuuksRERFq2rSpbrjhBqWlpVnvG2P05JNPKjo6WqGhoRo0aJC+/PJLr33k5+dr0qRJatWqlZo1a6bRo0fr0KFDXm1ycnKUmJgol8sll8ulxMREnTp1yo5TBAAAAcavA1hOTo5uvPFGNWrUSP/+97+1c+dO/elPf1KLFi2sNvPmzdPzzz+vRYsWacuWLYqKitKtt96q06dPW22SkpK0fPlyLVu2TBs2bNCZM2c0cuRIFRcXW23Gjh2r9PR0rVy5UitXrlR6eroSExPtPF0Line truncated
|
||||||
"text/plain": [
|
"text/plain": [
|
||||||
"<Figure size 640x480 with 1 Axes>"
|
"<Figure size 640x480 with 1 Axes>"
|
||||||
]
|
]
|
||||||
@@ -444,7 +478,7 @@
|
|||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"source": [
|
"source": [
|
||||||
"That makes it clear that there is a strong linear relation between number of backtracks and run time (with a couple of outliers).\n",
|
"This plot makes it clear that there is a strong linear relation between number of backtracks and run time. (Very roughly, one microsecond per backtrack.)\n",
|
||||||
"\n",
|
"\n",
|
||||||
"One weakness of a scatter plot as a visualization tool is that there can be lots of points plotted on top of each other, and you can't tell the density of such points. A histogram portrays density better (but on only one attribute at a time):"
|
"One weakness of a scatter plot as a visualization tool is that there can be lots of points plotted on top of each other, and you can't tell the density of such points. A histogram portrays density better (but on only one attribute at a time):"
|
||||||
]
|
]
|
||||||
@@ -466,7 +500,7 @@
|
|||||||
},
|
},
|
||||||
{
|
{
|
||||||
"data": {
|
"data": {
|
||||||
"image/png": "iVBORw0KGgoAAAANSUhEUgAAAjIAAAGxCAYAAAB4AFyyAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjYsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvq6yFwwAAAAlwSFlzAAAPYQAAD2EBqD+naQAAKE9JREFUeJzt3X90VPWd//HXECYDYZNoyBIISSCe065iBCRJKfgDUgUaERtsLVtshBb3LJugpFlXUbZtYGVDv7vrYbsOtNhuOVuLsKzCupYVx0V+tKD8TAVzui270SASIlQzQNYwTD7fP7qZZSYBmeTODZ/k+Tgnh947n7zvZ94zZl69c394jDFGAAAAFhrQ2xMAAADoLoIMAACwFkEGAABYiyADAACsRZABAADWIsgAAABrEWQAAIC1CDIAAMBaBBkAAGAtggwAALAWQQYAAFiLIAMAAKxFkAHgiPnz52v06NGd1tfU1Mjj8USWN23apIkTJyo9PV0pKSm64YYb9M1vfjPqd4LBoB577DHl5+crOTlZI0eOVFVVlc6fPx81rr29Xf/wD/+g8ePHa/Dgwbruuuv0+c9/Xi+//HJCniOAa8/A3p4AgP5j7969mjNnjubMmaOamhoNGjRI7733nrZv3x4Z09raqilTpuj999/XU089pbFjx+qdd97Rd77zHR05ckSvv/56JBjNnz9fzz//vBYsWKDly5crOTlZhw4d0rvvvttLzxCA2wgyAFyzZ88eGWP0gx/8QOnp6ZH18+fPj/zv73//+3r77bf11ltvqaioSJJ01113aeTIkfrKV76iV199VaWlpdq9e7d++tOfaunSpXr66acjv//FL37RtecDoPfx1RIA1xQXF0uSvvrVr+qf//mfdeLEiU5jXnnlFRUUFGj8+PG6ePFi5GfGjBnyeDzasWOHJOnf//3fJUmVlZWuzR/AtYcgA8A1d955p7Zs2aKLFy/qoYceUk5OjgoKCvTCCy9Expw6dUpvv/22vF5v1E9qaqqMMTp9+rQk6cMPP1RSUpKGDx/eW08HwDWAr5YAOObixYud1p07dy5q+Utf+pK+9KUvqa2tTW+++aZqa2s1d+5cjR49WpMmTVJmZqYGDx6sf/zHf+xyG5mZmZKkP/zDP1Q4HFZTU5NGjBjh/JMBYAX2yABwzMmTJ9Xc3By17pe//GWXY30+n6ZMmaLvfe97kqTDhw9Lku69917913/9l4YOHaqioqJOPx1nRpWWlkqS1qxZk6BnA8AG7JEB4BiPx6OysjI98cQT8vl82rBhgw4dOiRJev755/XWW2/p/Pnzuuuuu5STk6OPP/5Yf//3fy+v16spU6ZIkqqqqvTiiy/qzjvv1Le+9S2NHTtW7e3tamxs1GuvvaY///M/18SJE3XHHXeovLxcTz/9tE6dOqV7771XPp9Phw8fVkpKih555JHebAUAlxBkADgmJydHZWVl+tM//VO1tLTo7rvv1vbt2/XVr35VS5Ys0fe+9z397Gc/0xNPPKEPP/xQ1113nYqKirR9+3bdfPPNkqQhQ4Zo9+7dWrlypdauXauGhgYNHjxYeXl5uvvuu6OuVbNu3TpNmDBBP/7xj7Vu3ToNHjxYY8aM0VNPPdVLHQDgNo8xxvT2JADYb/78+dqxYwfXcAHgKo6RAQAA1iLIAAAAa/HVEgAAsBZ7ZAAAgLUIMgAAwFoEGQAAYC3rriPT3t6uDz74QKmpqfJ4PL09HQAAcBWMMTp79qyys7M1YIBz+1GsCzIffPCBcnNze3saAACgG44fP66cnBzH6lkTZPx+v/x+f+SmdMePH1daWpojtUOhkF577TVNnz5dXq/XkZq4MnruPnruPnruLvrtvnh6HgwGlZubq9TUVEfnYE2QqaysVGVlpYLBoNLT05WWluZokElJSVFaWhpvfpfQc/fRc/fRc3fRb/d1p+dOHxbCwb4AAMBaBBkAAGAta4KM3+/XmDFjVFxc3NtTAQAA1whrgkxlZaXq6+u1f//+3p4KAAC4RlgTZAAAAGIRZAAAgLUIMgAAwFrWBBkO9gUAALGsCTIc7AsAAGJZE2QAAABiEWQAAIC1CDIAAMBaBBkAAGAta+5+7ff75ff7FQ6HE7qd0Ut+7mi9d1fOdLQeAAD4P9bskeGsJQAAEMuaIAMAABCLIAMAAKxFkAEAANYiyAAAAGsRZAAAgLWsCTLcNBIAAMSyJshw+jUAAIhlTZABAACIRZABAADWIsgAAABrEWQAAIC1CDIAAMBaBBkAAGAtggwAALCWNUGGC+IBAIBY1gQZLogHAABiWRNkAAAAYhFkAACAtQgyAADAWgQZAABgLYIMAACwFkEGAABYiyADAACsRZABAADWIsgAAABrEWQAAIC1rAky3GsJAADEsibIcK8lAAAQy5ogAwAAEIsgAwAArEWQAQAA1iLIAAAAaxFkAACAtQgyAADAWgQZAABgLYIMAACwFkEGAABYiyADAACsRZABAADWIsgAAABrEWQAAIC1CDIAAMBavRZkWltbNWrUKD322GO9NQUAAGC5XgsyK1as0MSJE3tr8wAAoA/olSDz29/+Vr/+9a91zz339MbmAQBAHxF3kNm1a5dmzZql7OxseTwebdmypdOY1atXKz8/X4MGDVJhYaF2794d9fhjjz2m2trabk8aAABA6kaQOX/+vMaNG6dnn322y8c3btyoqqoqLV26VIcPH9Ydd9yh0tJSNTY2SpL+9V//VZ/97Gf12c9+tmczBwAA/d7AeH+htLRUpaWll338mWee0YIFC/Twww9LklatWqVt27ZpzZo1qq2t1ZtvvqkNGzZo06ZNOnfunEKhkNLS0vSd73yny3ptbW1qa2uLLAeDQUlSKBRSKBSKd/pd6qgTCoXkSzKO1IytjWiX9hzuoOfuo+fuot/ui6fniXpdPMaYbn9yezwebd68WWVlZZKkCxcuKCUlRZs2bdLs2bMj4xYvXqy6ujrt3Lkz6vfXrVuno0eP6m//9m8vu42amhotW7as0/r169crJSWlu1MHAAAuam1t1dy5c9XS0qK0tDTH6sa9R+ZKTp8+rXA4rKysrKj1WVlZampq6lbNJ598UtXV1ZHlYDCo3NxcTZ8+3bFGhEIhBQIBTZs2Tbeu2O5IzQ5Ha2Y4Wq+vuLTnXq+3t6fTL9Bz99Fzd9Fv98XT845vVJzmaJDp4PF4opaNMZ3WSdL8+fM/tZbP55PP5+u03uv1Ov5G9Xq9agt3nmdPa+LyEvE64sroufvoubvot/uupueJek0cPf06MzNTSUlJnfa+NDc3d9pLEy+/368xY8aouLi4R3UAAEDf4WiQSU5OVmFhoQKBQNT6QCCgyZMn96h2ZWWl6uvrtX///h7VAQAAfUfcXy2dO3dOx44diyw3NDSorq5OGRkZysvLU3V1tcrLy1VUVKRJkyZp7dq1amxs1MKFCx2dOAAAQNxB5sCBAyopKYksdxyIO2/ePK1bt05z5szRmTNntHz5cp08eVIFBQXaunWrRo0a5dysAQAA1I0gM3XqVH3aGdsVFRWqqKjo9qS64vf75ff7FQ6HHa0LAADs1Ws3jYwXx8gAAIBY1gQZAACAWAQZAABgLWuCDNeRAQAAsawJMhwjAwAAYlkTZAAAAGIRZAAAgLUIMgAAwFrWBBkO9gUAALGsCTIc7AsAAGJZE2QAAABiEWQAAIC1CDIAAMBa1gQZDvYFAACxrAkyHOwLAABiWRNkAAAAYhFkAACAtQgyAADAWgQZAABgLYIMAACwljVBhtOvAQBALGuCDKdfAwCAWNYEGQAAgFgEGQAAYC2CDAAAsBZBBgAAWIsgAwAArEWQAQAA1iLIAAAAa1kTZLggHgAAiGVNkOGCeAAAIJY1QQYAACAWQQYAAFiLIAMAAKxFkAEAANYiyAAAAGsRZAAAgLUIMgAAwFoEGQAAYC2CDAAAsBZBBgAAWIsgAwAArGVNkOGmkQAAIJY1QYabRgIAgFjWBBkAAIBYBBkAAGAtggwAALAWQQYAAFiLIAMAAKxFkAEAANYiyAAAAGsRZAAAgLUIMgAAwFoEGQAAYC2CDAAAsBZBBgAAWIsgAwAArEWQAQAA1nI9yJw9e1bFxcUaP368brnlFj333HNuTwEAAPQRA93eYEpKinbu3KmUlBS1traqoKBA999/v4YOHer2VAAAgOVc3yOTlJSklJQUSdInn3yicDgsY4zb0wAAAH1A3EFm165dmjVrlrKzs+XxeLRly5ZOY1avXq38/HwNGjRIhYWF2r17d9TjH3/8scaNG6ecnBw9/vjjyszM7PYTAAAA/VfcQeb8+fMaN26cnn322S4f37hxo6qqqrR06VIdPnxYd9xxh0pLS9XY2BgZc9111+lXv/qVGhoatH79ep06dar7zwAAAPRbcR8jU1paqtLS0ss+/swzz2jBggV6+OGHJUmrVq3Stm3btGbNGtXW1kaNzcrK0tixY7Vr1y498MADXdZra2tTW1tbZDkYDEqSQqGQQqFQvNPvUkedUCgkX5KzX3M5Nce+5tKewx303H303F30233x9DxRr4vH9OAAFY/Ho82bN6usrEySdOHCBaWkpGjTpk2aPXt2ZNzixYtVV1ennTt36tSpUxo8eLDS0tIUDAY1adIkvfDCCxo7dmyX26ipqdGyZcs6rV+/fn3kWBsAAHBta21t1dy5c9XS0qK0tDTH6jp61tLp06cVDoeVlZUVtT4rK0tNTU2SpPfff18LFiyQMUbGGC1atOiyIUaSnnzySVVXV0eWg8GgcnNzNX36dMcaEQqFFAgENG3aNN26YrsjNTscrZnhaL2+4tKee73e3p5Ov0DP3UfP3UW/3RdPzzu+UXFaQk6/9ng8UcvGmMi6wsJC1dXVXXUtn88nn8/Xab3X63X8jer1etUW9nz6wDhr4vIS8Triyui5++i5u+i3+66m54l6TRw9/TozM1NJSUmRvS8dmpubO+2liZff79eLine truncated
|
"image/png": "iVBORw0KGgoAAAANSUhEUgAAAicAAAGxCAYAAAC5hxYeAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjYsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvq6yFwwAAAAlwSFlzAAAPYQAAD2EBqD+naQAAKIVJREFUeJzt3X90VPWd//HXECYDYZNoyBIISSCe067GCEiSUvAHUAUaERvsD7bYCC3uWTZBSbOuouy3Daxs6P7wsF0HWmy3nK1FWFZhXWWL4yI/WlB+poI53ZbdaBAJEaoZIGsYJp/vH/1mvoyJwJA7k8/NPB/n5BzunU/e93PfGZLXuXN/eIwxRgAAAJYY0NcTAAAAuBThBAAAWIVwAgAArEI4AQAAViGcAAAAqxBOAACAVQgnAADAKoQTAABgFcIJAACwCuEEAABYhXACAACsQjgBAABWIZwAcMT8+fM1evTobuvr6urk8Xgiy5s2bdKECROUmZmptLQ03XDDDfrWt74V9T3BYFCPPvqoCgsLlZqaqpEjR6qmpkbnz5+PGtfZ2al//Md/1Lhx4zR48GBdd911+vznP6+XXnopLvsIIDEG9vUEACSPvXv3as6cOZozZ47q6uo0aNAgvfvuu9q+fXtkTHt7uyZPnqz33ntPTz75pMaMGaO3335b3/nOd3TkyBG99tprkbAzf/58Pffcc1qwYIGWL1+u1NRUHTp0SO+8804f7SEAJxBOACTMnj17ZIzRD37wA2VmZkbWz58/P/Lv73//+3rrrbf05ptvqrS0VJJ01113aeTIkfrKV76in//85yovL9fu3bv105/+VEuXLtVTTz0V+f4vfvGLCdsfAPHBxzoAEqasrEyS9LWvfU3/8i//ohMnTnQb8/LLL6u4uFjjxo3TxYsXI18zZsyQx+PRjh07JEn/8R//IUmqrq5O2PwBJAbhBEDC3HnnndqyZYsuXryoBx98UHl5eSouLtbzzz8fGXPq1Cm99dZb8nq9UV/p6ekyxuj06dOSpA8++EApKSkaPnx4X+0OgDjhYx0Ajrl48WK3defOnYta/tKXvqQvfelL6ujo0BtvvKH6+nrNnTtXo0eP1sSJE5Wdna3Bgwfrn/7pn3rcRnZ2tiTpD//wDxUOh9XS0qIRI0Y4vzMA+gxHTgA45uTJk2ptbY1a98tf/rLHsT6fT5MnT9b3vvc9SdLhw4clSffee6/++7//W0OHDlVpaWm3r64rgsrLyyVJa9asidPeAOgrHDkB4BiPx6OKigo9/vjj8vl82rBhgw4dOiRJeu655/Tmm2/q/Pnzuuuuu5SXl6ePPvpI//AP/yCv16vJkydLkmpqavTCCy/ozjvv1Le//W2NGTNGnZ2dam5u1quvvqo///M/14QJE3THHXeosrJSTz31lE6dOqV7771XPp9Phw8fVlpamh5++OG+bAWAXiCcAHBMXl6eKioq9Kd/+qdqa2vT3Xffre3bt+trX/ualixZou9973v62c9+pscff1wffPCBrrvuOpWWlmr79u26+eabJUlDhgzR7t27tXLlSq1du1ZNTU0aPHiwCgoKdPfdd0fdS2XdunUaP368fvzjH2vdunUaPHiwioqK9OSTT/ZRBwA4wWOMMX09CQDuN3/+fO3YsYN7jADoNc45AQAAViGcAAAAq/CxDgAAsApHTgAAgFUIJwAAwCqEEwAAYBXX3eeks7NT77//vtLT0yOPTQcAAHYzxujs2bPKzc3VgAGXPzbiunDy/vvvKz8/v6+nAQAArsHx48eVl5d32TGuCSd+v19+vz/yYLHjx48rIyPDkdqhUEivvvqqpk+fLq/X60hNdEefE4M+xx89Tgz6nBiJ6nMwGFR+fr7S09OvONY14aS6ulrV1dUKBoPKzMxURkaGo+EkLS1NGRkZ/AeII/qcGPQ5/uhxYtDnxEh0n6/mlAxOiAUAAFYhnAAAAKu4Jpz4/X4VFRWprKysr6cCAADiyDXhpLq6Wo2Njdq/f39fTwUAAMSRa8IJAABIDoQTAABgFcIJAACwimvCCSfEAgCQHFwTTjghFgCA5OCacAIAAJID4QQAAFiFcAIAAKxCOAEAAFZxzVOJ/X6//H6/wuFwXLczeskrjtZ7Z+VMR+sBANDfuebICVfrAACQHFwTTgAAQHIgnAAAAKsQTgAAgFUIJwAAwCqEEwAAYBXXhBMe/AcAQHJwTTjhUmIAAJKDa8IJAABIDoQTAABgFcIJAACwCuEEAABYhXACAACsQjgBAABWIZwAAACruCaccBM2AACSg2vCCTdhAwAgObgmnAAAgORAOAEAAFYhnAAAAKsQTgAAgFUIJwAAwCqEEwAAYBXCCQAAsArhBAAAWIVwAgAArEI4AQAAVnFNOOHZOgAAJAfXhBOerQMAQHJwTTgBAADJgXACAACsQjgBAABWIZwAAACrEE4AAIBVCCcAAMAqhBMAAGAVwgkAALAK4QQAAFiFcAIAAKxCOAEAAFYhnAAAAKsQTgAAgFUIJwAAwCp9Fk7a29s1atQoPfroo301BQAAYKE+CycrVqzQhAkT+mrzAADAUn0STn7729/q17/+te65556+2DwAALBYzOFk165dmjVrlnJzc+XxeLRly5ZuY1avXq3CwkINGjRIJSUl2r17d9Trjz76qOrr66950gAAoP+KOZycP39eY8eO1TPPPNPj6xs3blRNTY2WLl2qw4cP64477lB5ebmam5slSf/2b/+mz372s/rsZz/bu5kDAIB+aWCs31BeXq7y8vJPff3pp5/WggUL9NBDD0mSVq1apW3btmnNmjWqr6/XG2+8oQ0bNmjTpk06d+6cQqGQMjIy9J3vfKfHeh0dHero6IgsB4NBSVIoFFIoFIp1+j3qqhMKheRLMY7U/GRtRPcZ8UOf448eJwZ9ToxE9TmW+h5jzDX/NfZ4PNq8ebMqKiokSRcuXFBaWpo2bdqk2bNnR8YtXrxYDQ0N2rlzZ9T3r1u3TkePHtXf/d3ffeo26urqtGzZsm7r169fr7S0tGudOgAASKD29nbNnTtXbW1tysjIuOzYmI+cXM7p06cVDoeVk5MTtT4nJ0ctLS3XVPOJJ55QbW1tZDkYDCo/P1/Tp0+/4s5drVAopEAgoGnTpunWFdsdqdnlaN0MR+u52aV99nq9fT2dfos+xx89Tgz6nBiJ6nPXJx9Xw9Fw0sXj8UQtG2O6rZOk+fPnX7GWz+eTz+frtt7r9TreRK/Xq45w93n2tiaixeNnh+7oc/zR48Sgz4kR7z7HUtvRS4mzs7OVkpLS7ShJa2trt6MpsfL7/SoqKlJZWVmv6gAAALs5Gk5SU1NVUlKiQCAQtT4QCGjSpEm9ql1dXa3Gxkbt37+/V3UAAIDdYv5Y59y5czp27FhkuampSQ0NDcrKylJBQYFqa2tVWVmp0tJSTZw4UWvXrlVzc7MWLlzo6MQBAED/FHM4OXDggKZOnRpZ7jpZdd68eVq3bp3mzJmjM2fOaPny5Tp58qSKi4u1detWjRo1yrlZAwCAfivmcDJlyhRd6erjqqoqVVVVXfOkeuL3++X3+xUOhx2tCwAA7NJnD/6LFeecAACQHFwTTgAAQHIgnAAAAKu4JpxwnxMAAJKDa8IJ55wAAJAcXBNOAABAciCcAAAAqxBOAACAVVwTTjghFgCA5OCacMIJsQAAJAfXhBMAAJAcCCcAAMAqhBMAAGAV14QTTogFACA5uCaccEIsAADJwTXhBAAAJAfCCQAAsArhBAAAWIVwAgAArEI4AQAAVnFNOOFSYgAAkoNrwgmXEgMAkBxcE04AAEByIJwAAACrEE4AAIBVCCcAAMAqhBMAAGAVwgkAALAK4QQAAFjFNeGEm7ABAJAcXBNOuAkbAADJwTXhBAAAJAfCCQAAsArhBAAAWIVwAgAArEI4AQAAViGcAAAAqxBOAACAVQgnAADAKoQTAABgFcIJAACwCuEEAABYxTXhhAf/AQCQHFwTTnjwHwAAycE14QQAACQHwgkAALAK4QQAAFiFcAIAAKxCOAEAAFYhnAAAAKsQTgAAgFUIJwAAwCqEEwAAYBXCCQAAsArhBAAAWIVwAgAArEI4AQAAViGcAAAAqyQ8nJw9e1ZlZWUaN26cbrnlFj377LOJngIAALDYwERvMC0tTTt37lRaWpra29tVXFys+++/X0OHDk30VAAAgIUSfuQkJSVFaWlpkqSPP/5Y4XBYxphETwMAAFgq5nCya9cuzZo1S7m5ufJ4PNqyZUu3MatXr1ZhYaEGDRqkkpIS7d69O+r1jz76SGPHjlVeXp4ee+wxZWdnX/MOAACA/iXmcHL+/HmNHTtWzzzzTI+vb9y4UTU1NVq6dKkOHz6sO+64Q+Xl5Wpubo6Mue666/SrX/1KTU1NWr9+vU6dOnXtewAAAPqVmM85KS8vV3l5+ae+/vTTT2vBggV66KGHJEmrVq3Stm3btGbNGtXX10eNzcnJ0ZgxY7Rr1y599atf7bFeR0eHOjo6IsvBYFCSFAqFFAqFYp1+j7rqhEIh+VKc/YjJqTn2B5f2GfFDn+OPHicGfU6MRPU5lvoe04sTPjwejzZv3qyKigpJ0oULF5SWlqZNmzZp9uzZkXGLFy9WQ0ODdu7cqVOnTmnw4MHKyMhQMBjUxIkT9fzzz2vMmDE9bqOurk7Lli3rtn79+vWRc1cAAIDd2tvbNXfuXLW1tSkjI+OyYx29Wuf06dMKh8PKycmJWp+Tk6OWlhZJ0nvvvacFCxbIGCNjjBYtWvSpwUSSnnjiCdXW1kaWg8Gg8vPzNX369Cvu3NUKhUIKBAKaNm2abl2x3ZGaXY7WzXC0nptd2mev19vX0+m36HP80ePEoM+Jkag+d33ycTXicimxx+OJWjbGRNaVlJSooaHhqmv5fD75fL5u671er+NN9Hq96gh7rjwwxpqIFo+fHbqjz/FHjxODPidGvPscS21HLyXOzs5WSkpK5ChJl9bLine truncated
|
||||||
"text/plain": [
|
"text/plain": [
|
||||||
"<Figure size 640x480 with 1 Axes>"
|
"<Figure size 640x480 with 1 Axes>"
|
||||||
]
|
]
|
||||||
@@ -524,7 +558,7 @@
|
|||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"source": [
|
"source": [
|
||||||
"# Verifying Correctness\n",
|
"# Is the Program Correct?\n",
|
||||||
"\n",
|
"\n",
|
||||||
"How do we know this program (or any program) is correct? Traditionally, there are four kinds of evidence:\n",
|
"How do we know this program (or any program) is correct? Traditionally, there are four kinds of evidence:\n",
|
||||||
"- A large number of example input/output pairs that give the right answer.\n",
|
"- A large number of example input/output pairs that give the right answer.\n",
|
||||||
@@ -705,13 +739,14 @@
|
|||||||
"\n",
|
"\n",
|
||||||
"There are a few things I didn't get a chance to explore; maybe you can:\n",
|
"There are a few things I didn't get a chance to explore; maybe you can:\n",
|
||||||
"\n",
|
"\n",
|
||||||
"- Would the program be even faster in Golang or C++ or Rust?\n",
|
|
||||||
"- Are there more algorithmic optimizations to try?\n",
|
"- Are there more algorithmic optimizations to try?\n",
|
||||||
|
"- Would the program be even faster if translated to Golang or C++ or Rust?\n",
|
||||||
|
"- Could you use a satisfiability prover such as DPLL to solve puzzles, as [[**tdoku**](https://github.com/t-dillon/tdoku) does?\n",
|
||||||
"- The depth-first search makes a choice to *fill* some square with a digit. What if instead the choice was to *eliminate* a digit from the square? At first glance it seems that would be slower, because more choices would be required, but would constraint propagation make it work well?\n",
|
"- The depth-first search makes a choice to *fill* some square with a digit. What if instead the choice was to *eliminate* a digit from the square? At first glance it seems that would be slower, because more choices would be required, but would constraint propagation make it work well?\n",
|
||||||
"- On each recursive call, the depth-first search copies the current grid into a new grid (re-using the one in `gridpool[level]`). That requires copying an array of 81 ints. Would it be faster to instead make changes directly to the current grid, and then undo the changes when failure is detected? You would need to keep track of the changes made so that they can be undone. My guess is that this would make the code more complex and not much faster (if any), but you might want to try it.\n",
|
"- On each recursive call, the depth-first search copies the current grid into a new grid (re-using the one in `gridpool[level]`). That requires copying an array of 81 ints. Would it be faster to instead make changes directly to the current grid, and then undo the changes when failure is detected? You would need to keep track of the changes made so that they can be undone. My guess is that this would make the code more complex and not much faster (if any), but you might want to try it.\n",
|
||||||
"- In the theory of constraint propagation, [shaving](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.175.7143&rep=rep1&type=pdf) means guessing a value for some variable, detecting a contradiction, and then keeping track of the fact that the value is not possible. But in our program, when we guess wrong we don't keep track of anything. Can the program be made faster by incorporating shaving?\n",
|
"- In the theory of constraint propagation, [shaving](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.175.7143&rep=rep1&type=pdf) means guessing a value for some variable, detecting a contradiction, and then keeping track of the fact that the value is not possible. But in our program, when we guess wrong we don't keep track of anything. Can the program be made faster by incorporating shaving?\n",
|
||||||
"- Can you create an adversarial puzzle, where the program guesses wrong the maximal number of times? In other words, if you draw a tree of choices, what's a puzzle with a tree that has the solution in the bottom-right corner? How much time and how many backtracks does that puzzle take to solve?\n",
|
"- Can you create an adversarial puzzle, where the program guesses wrong the maximal number of times? In other words, if you draw a tree of choices, what's a puzzle with a tree that has the solution in the bottom-right corner? How much time and how many backtracks does that puzzle take to solve?\n",
|
||||||
"- What [other Sudoku strategies](https://bestofsudoku.com/sudoku-strategy) can be implemented? Can you find a suite of strategies that will solve all the puzzles with no search? \n",
|
"- What [other Sudoku strategies](https://bestofsudoku.com/sudoku-strategy) can be implemented? Can you find a suite of strategies that will solve all the puzzles with no backtracking search? \n",
|
||||||
"- Can you develop a system to rank the difficulty of puzzles, based on the complexity of the strategies needed to solve it?\n"
|
"- Can you develop a system to rank the difficulty of puzzles, based on the complexity of the strategies needed to solve it?\n"
|
||||||
]
|
]
|
||||||
},
|
},
|
||||||
|
|||||||
Reference in new issue
Block a user