minor change

aeb9afaa · Michael Leuschel · 1e2d3db5 · aeb9afaa
Commit aeb9afaa authored May 22, 2020 by Michael Leuschel
--- a/puzzles/Sudoku_Miracle.ipynb
+++ b/puzzles/Sudoku_Miracle.ipynb
@@ -679,7 +679,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
@@ -688,14 +688,14 @@
       "Loaded machine: Sudoku_Horizontal_Vertical"
      ]
     },
-     "execution_count": 21,
+     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
-    "MACHINE Sudoku_Horizontal_Vertical\n",
+    "MACHINE Sudoku_Miracle\n",
    "DEFINITIONS DOM == 1..9; D1 == 1..8; D2 == 2..9;\n",
    "      SUBSQ == { {1,2,3}, {4,5,6}, {7,8,9} };\n",
    "      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};\n",
@@ -999,6 +999,31 @@
    ":dot state_space"
   ]
  },
+  {
+   "cell_type": "code",
+   "execution_count": 32,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "**Explored States:** 1/2  \n",
+       "**Transitions:** 1"
+      ],
+      "text/plain": [
+       "Explored States: 1/2\n",
+       "Transitions: 1"
+      ]
+     },
+     "execution_count": 32,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":stats"
+   ]
+  },
  {
   "cell_type": "code",
   "execution_count": null,

 %% Cell type:markdown id: tags:
 # Sudoku - The Miracle
 Here we show how to solve a variation of the Sudoku puzzle, called "The Miracle", desigen by Mitchell Lee.
 Some links are:
 * https://www.reddit.com/r/sudoku/comments/ghkkwp/the_miracle_sudoku/
 * https://www.youtube.com/watch?v=yKf9aUIxdb4 */
 * https://www.popularmechanics.com/science/a32605317/miracle-sudoku-hardest-puzzle-ever/
 In this puzzle the standard Sudoku rules apply, but in addition there are additional constraints.
 The puzzle states that in row 5 and column 3 there is a 1 and in row 6 at column 7 a 2.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Sudoku_Setup
 DEFINITIONS DOM == 1..9;
      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};
      ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM &  i = Board(r)(c)} );
      ANIMATION_IMG0 == "images/sm_empty_box.gif";
      ANIMATION_IMG1 == "images/sm_1.gif";
      ANIMATION_IMG2 == "images/sm_2.gif";
      ANIMATION_IMG3 == "images/sm_3.gif";
      ANIMATION_IMG4 == "images/sm_4.gif";
      ANIMATION_IMG5 == "images/sm_5.gif";
      ANIMATION_IMG6 == "images/sm_6.gif";
      ANIMATION_IMG7 == "images/sm_7.gif";
      ANIMATION_IMG8 == "images/sm_8.gif";
      ANIMATION_IMG9 == "images/sm_9.gif"
 CONSTANTS Board
 PROPERTIES
  Board : DOM +-> (DOM +-> DOM)   &
 /* PUZZLE CONSTRAINTS : */
   Board(5)(3)=1 & Board(6)(7)=2
 END
 ```
 %% Output
    Loaded machine: SudokuAsConstantMiracle
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    Machine initialised using operation 1: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    <td style="padding:0px"><img alt="0" src="images/sm_empty_box.gif"/></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:markdown id: tags:
 Let us gradually solve this puzzle. First we need to stipulate that ```Board``` is totally defined over the domain of numbers from 1..9 and that on all columns and rows the numbers must be distinct.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Sudoku_Horizontal_Vertical
 DEFINITIONS DOM == 1..9; D1 == 1..8; D2 == 2..9;
      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};
      ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM &  i = Board(r)(c)} );
      ANIMATION_IMG0 == "images/sm_empty_box.gif";
      ANIMATION_IMG1 == "images/sm_1.gif";
      ANIMATION_IMG2 == "images/sm_2.gif";
      ANIMATION_IMG3 == "images/sm_3.gif";
      ANIMATION_IMG4 == "images/sm_4.gif";
      ANIMATION_IMG5 == "images/sm_5.gif";
      ANIMATION_IMG6 == "images/sm_6.gif";
      ANIMATION_IMG7 == "images/sm_7.gif";
      ANIMATION_IMG8 == "images/sm_8.gif";
      ANIMATION_IMG9 == "images/sm_9.gif"
 CONSTANTS Board
 PROPERTIES
  Board ∈ DOM --> (DOM --> DOM)
  ∧
  /*@label "Horizontal and vertical lines" */
  ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2  ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧
                                                    Board(y)(x1) ≠ Board(y)(x2))))
     /*@desc "within a vertical or horizontal line all numbers must be different" */
  ∧
 /* PUZZLE CONSTRAINTS : */
   Board(5)(3)=1 ∧ Board(6)(7)=2
 END
 ```
 %% Output
    Loaded machine: Sudoku_Horizontal_Vertical
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    Machine initialised using operation 1: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:markdown id: tags:
 Now let us stipulate that within each sub-square the numbers must also be distinct.
 For this we introduce the possible indices for the subsquares ```SUBSQ```.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Sudoku_Horizontal_Vertical
 DEFINITIONS DOM == 1..9; D1 == 1..8; D2 == 2..9;
      SUBSQ == { {1,2,3}, {4,5,6}, {7,8,9} };
      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};
      ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM &  i = Board(r)(c)} );
      ANIMATION_IMG0 == "images/sm_empty_box.gif";
      ANIMATION_IMG1 == "images/sm_1.gif";
      ANIMATION_IMG2 == "images/sm_2.gif";
      ANIMATION_IMG3 == "images/sm_3.gif";
      ANIMATION_IMG4 == "images/sm_4.gif";
      ANIMATION_IMG5 == "images/sm_5.gif";
      ANIMATION_IMG6 == "images/sm_6.gif";
      ANIMATION_IMG7 == "images/sm_7.gif";
      ANIMATION_IMG8 == "images/sm_8.gif";
      ANIMATION_IMG9 == "images/sm_9.gif"
 CONSTANTS Board
 PROPERTIES
  Board : DOM --> (DOM --> DOM)
  ∧
  /*@label "Horizontal and vertical lines" */
  ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2  ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧
                                                    Board(y)(x1) ≠ Board(y)(x2))))
     /*@desc "within a vertical or horizontal line all numbers must be different" */
  ∧
  /*@label "Squares" */
  ∀(s1,s2).(s1:SUBSQ ∧ s2:SUBSQ ⇒
             ∀(x1,y1,x2,y2).( (x1∈s1 ∧ x2∈s1 ∧
                               x1>=x2 ∧ (x1=x2 ⇒ y1>y2) ∧ // lexicographical ordering
                               y1∈s2 ∧ y2∈s2 ∧ (x1,y1) ≠ (x2,y2))
                              ⇒
                              Board(x1)(y1) ≠ Board(x2)(y2)
                            ))
     /*@desc "within a sub-square all numbers must be different" */
    ∧
 /* PUZZLE CONSTRAINTS : */
   Board(5)(3)=1 ∧ Board(6)(7)=2
 END
 ```
 %% Output
    Loaded machine: Sudoku_Horizontal_Vertical
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    Machine initialised using operation 1: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:markdown id: tags:
 Now we found a classical Sudoku solution.
 We now also add the following constraints:
 * Any two cells separated by a knight's or king's move (in chess) cannot contain the same digit
 * Any two orthogonally adjacent cells cannot contain consecutive digits.
 %% Cell type:code id: tags:
 ``` prob
 ::load
-MACHINE Sudoku_Horizontal_Vertical
+MACHINE Sudoku_Miracle
 DEFINITIONS DOM == 1..9; D1 == 1..8; D2 == 2..9;
      SUBSQ == { {1,2,3}, {4,5,6}, {7,8,9} };
      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};
      ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM &  i = Board(r)(c)} );
      ANIMATION_IMG0 == "images/sm_empty_box.gif";
      ANIMATION_IMG1 == "images/sm_1.gif";
      ANIMATION_IMG2 == "images/sm_2.gif";
      ANIMATION_IMG3 == "images/sm_3.gif";
      ANIMATION_IMG4 == "images/sm_4.gif";
      ANIMATION_IMG5 == "images/sm_5.gif";
      ANIMATION_IMG6 == "images/sm_6.gif";
      ANIMATION_IMG7 == "images/sm_7.gif";
      ANIMATION_IMG8 == "images/sm_8.gif";
      ANIMATION_IMG9 == "images/sm_9.gif"
 CONSTANTS Board
 PROPERTIES
  Board : DOM --> (DOM --> DOM)
  ∧
  /*@label "Horizontal and vertical lines" */
  ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2  ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧
                                                    Board(y)(x1) ≠ Board(y)(x2))))
     /*@desc "within a vertical or horizontal line all numbers must be different" */
  ∧
  /*@label "Squares" */
  ∀(s1,s2).(s1:SUBSQ ∧ s2:SUBSQ ⇒
             ∀(x1,y1,x2,y2).( (x1∈s1 ∧ x2∈s1 ∧
                               x1>=x2 ∧ (x1=x2 ⇒ y1>y2) ∧ // lexicographical ordering
                               y1∈s2 ∧ y2∈s2 ∧ (x1,y1) ≠ (x2,y2))
                              ⇒
                              Board(x1)(y1) ≠ Board(x2)(y2)
                            ))
     /*@desc "within a sub-square all numbers must be different" */
  ∧
    /*@label "King Moves" */
  ∀(x,y).(x∈D2 ∧ y∈D2  ⇒
                          (Board(x)(y)   ≠ Board(x-1)(y-1) ∧
                           Board(x)(y-1) ≠ Board(x-1)(y) )
    )
  ∧
  /*@label "Orthogonals" */
  ∀(x,y).(x∈D1 ∧ y∈DOM  ⇒
                          (  Board(x)(y) ≠ 1+Board(x+1)(y) ∧
                           1+Board(x)(y) ≠   Board(x+1)(y) ∧
                             Board(y)(x) ≠ 1+Board(y)(x+1) ∧
                           1+Board(y)(x) ≠   Board(y)(x+1) )
    )
     /*@desc "any two orthogonally adjacent cells cannot contain consecutive digits" */
  ∧
  /*@label "Knight Moves 1" */
  ∀(x,y).(x∈D1 ∧ y∈DOM  ⇒
                          ( y+2∈DOM ⇒ Board(x)(y) ≠ Board(x+1)(y+2)  ) ∧
                          ( y-2∈DOM ⇒ Board(x)(y) ≠ Board(x+1)(y-2)  )
    )
  ∧
  /*@label "Knight Moves 2" */
  ∀(x,y).(x∈1..7 ∧ y∈DOM  ⇒
                          ( y+1∈DOM ⇒ Board(x)(y) ≠ Board(x+2)(y+1)  ) ∧
                          ( y-1∈DOM ⇒ Board(x)(y) ≠ Board(x+2)(y-1)  )
    )
   ∧
 /* PUZZLE CONSTRAINTS : */
   Board(5)(3)=1 ∧ Board(6)(7)=2
 END
 ```
 %% Output
    Loaded machine: Sudoku_Horizontal_Vertical
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    Machine initialised using operation 1: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    </tr>
    <tr>
    <td style="padding:0px"><img alt="9" src="images/sm_9.gif"/></td>
    <td style="padding:0px"><img alt="4" src="images/sm_4.gif"/></td>
    <td style="padding:0px"><img alt="8" src="images/sm_8.gif"/></td>
    <td style="padding:0px"><img alt="3" src="images/sm_3.gif"/></td>
    <td style="padding:0px"><img alt="7" src="images/sm_7.gif"/></td>
    <td style="padding:0px"><img alt="2" src="images/sm_2.gif"/></td>
    <td style="padding:0px"><img alt="6" src="images/sm_6.gif"/></td>
    <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
    <td style="padding:0px"><img alt="5" src="images/sm_5.gif"/></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:markdown id: tags:
 This corresponds to the solution in https://www.youtube.com/watch?v=yKf9aUIxdb4
 We can see that there is only one solution:
 %% Cell type:code id: tags:
 ``` prob
 :dot state_space
 ```
 %% Output
    <Dot visualization: state_space []>
 %% Cell type:code id: tags:
 ``` prob
+:stats
+```
+%% Output
+    **Explored States:** 1/2
+    **Transitions:** 1
+    Explored States: 1/2
+    Transitions: 1
+%% Cell type:code id: tags:
+``` prob
 ```