diff --git a/puzzles/Sudoku_Miracle.ipynb b/puzzles/Sudoku_Miracle.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..751a788af1c46ce2f399137fd9c61d435593bf3c
--- /dev/null
+++ b/puzzles/Sudoku_Miracle.ipynb
@@ -0,0 +1,1025 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Sudoku - The Miracle\n",
+ "\n",
+ "\n",
+ "Here we show how to solve a variation of the Sudoku puzzle, called \"The Miracle\", desigen by Mitchell Lee.\n",
+ "Some links are:\n",
+ "* https://www.reddit.com/r/sudoku/comments/ghkkwp/the_miracle_sudoku/\n",
+ "* https://www.youtube.com/watch?v=yKf9aUIxdb4 */\n",
+ "* https://www.popularmechanics.com/science/a32605317/miracle-sudoku-hardest-puzzle-ever/\n",
+ "\n",
+ "In this puzzle the standard Sudoku rules apply, but in addition there are additional constraints.\n",
+ "The puzzle states that in row 5 and column 3 there is a 1 and in row 6 at column 7 a 2.\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: SudokuAsConstantMiracle"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Sudoku_Setup\n",
+ "DEFINITIONS DOM == 1..9;\n",
+ " ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};\n",
+ " ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM & i = Board(r)(c)} );\n",
+ " ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+ " ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+ " ANIMATION_IMG2 == \"images/sm_2.gif\";\n",
+ " ANIMATION_IMG3 == \"images/sm_3.gif\";\n",
+ " ANIMATION_IMG4 == \"images/sm_4.gif\";\n",
+ " ANIMATION_IMG5 == \"images/sm_5.gif\";\n",
+ " ANIMATION_IMG6 == \"images/sm_6.gif\";\n",
+ " ANIMATION_IMG7 == \"images/sm_7.gif\";\n",
+ " ANIMATION_IMG8 == \"images/sm_8.gif\";\n",
+ " ANIMATION_IMG9 == \"images/sm_9.gif\"\n",
+ "CONSTANTS Board\n",
+ "PROPERTIES\n",
+ " Board : DOM +-> (DOM +-> DOM) &\n",
+ "\n",
+ " /* PUZZLE CONSTRAINTS : */\n",
+ " Board(5)(3)=1 & Board(6)(7)=2\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "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",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Sudoku_Horizontal_Vertical"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Sudoku_Horizontal_Vertical\n",
+ "DEFINITIONS DOM == 1..9; D1 == 1..8; D2 == 2..9;\n",
+ " ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};\n",
+ " ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM & i = Board(r)(c)} );\n",
+ " ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+ " ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+ " ANIMATION_IMG2 == \"images/sm_2.gif\";\n",
+ " ANIMATION_IMG3 == \"images/sm_3.gif\";\n",
+ " ANIMATION_IMG4 == \"images/sm_4.gif\";\n",
+ " ANIMATION_IMG5 == \"images/sm_5.gif\";\n",
+ " ANIMATION_IMG6 == \"images/sm_6.gif\";\n",
+ " ANIMATION_IMG7 == \"images/sm_7.gif\";\n",
+ " ANIMATION_IMG8 == \"images/sm_8.gif\";\n",
+ " ANIMATION_IMG9 == \"images/sm_9.gif\"\n",
+ "CONSTANTS Board\n",
+ "PROPERTIES\n",
+ " Board ∈ DOM --> (DOM --> DOM)\n",
+ " ∧\n",
+ " /*@label \"Horizontal and vertical lines\" */\n",
+ " ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2 ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧\n",
+ " Board(y)(x1) ≠ Board(y)(x2))))\n",
+ " /*@desc \"within a vertical or horizontal line all numbers must be different\" */\n",
+ " ∧\n",
+ " /* PUZZLE CONSTRAINTS : */\n",
+ " Board(5)(3)=1 ∧ Board(6)(7)=2\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Now let us stipulate that within each sub-square the numbers must also be distinct.\n",
+ "For this we introduce the possible indices for the subsquares ```SUBSQ```."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Sudoku_Horizontal_Vertical"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Sudoku_Horizontal_Vertical\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",
+ " ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM & i = Board(r)(c)} );\n",
+ " ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+ " ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+ " ANIMATION_IMG2 == \"images/sm_2.gif\";\n",
+ " ANIMATION_IMG3 == \"images/sm_3.gif\";\n",
+ " ANIMATION_IMG4 == \"images/sm_4.gif\";\n",
+ " ANIMATION_IMG5 == \"images/sm_5.gif\";\n",
+ " ANIMATION_IMG6 == \"images/sm_6.gif\";\n",
+ " ANIMATION_IMG7 == \"images/sm_7.gif\";\n",
+ " ANIMATION_IMG8 == \"images/sm_8.gif\";\n",
+ " ANIMATION_IMG9 == \"images/sm_9.gif\"\n",
+ "CONSTANTS Board\n",
+ "PROPERTIES\n",
+ " Board : DOM --> (DOM --> DOM)\n",
+ " ∧\n",
+ " /*@label \"Horizontal and vertical lines\" */\n",
+ " ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2 ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧\n",
+ " Board(y)(x1) ≠ Board(y)(x2))))\n",
+ " /*@desc \"within a vertical or horizontal line all numbers must be different\" */\n",
+ " ∧\n",
+ " \n",
+ " /*@label \"Squares\" */\n",
+ " ∀(s1,s2).(s1:SUBSQ ∧ s2:SUBSQ ⇒\n",
+ " ∀(x1,y1,x2,y2).( (x1∈s1 ∧ x2∈s1 ∧ \n",
+ " x1>=x2 ∧ (x1=x2 ⇒ y1>y2) ∧ // lexicographical ordering\n",
+ " y1∈s2 ∧ y2∈s2 ∧ (x1,y1) ≠ (x2,y2))\n",
+ " ⇒\n",
+ " Board(x1)(y1) ≠ Board(x2)(y2)\n",
+ " ))\n",
+ " /*@desc \"within a sub-square all numbers must be different\" */\n",
+ " ∧\n",
+ " /* PUZZLE CONSTRAINTS : */\n",
+ " Board(5)(3)=1 ∧ Board(6)(7)=2\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Now we found a classical Sudoku solution.\n",
+ "\n",
+ "We now also add the following constraints:\n",
+ "* Any two cells separated by a knight's or king's move (in chess) cannot contain the same digit\n",
+ "* Any two orthogonally adjacent cells cannot contain consecutive digits.\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Sudoku_Horizontal_Vertical"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Sudoku_Horizontal_Vertical\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",
+ " ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM & i = Board(r)(c)} );\n",
+ " ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+ " ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+ " ANIMATION_IMG2 == \"images/sm_2.gif\";\n",
+ " ANIMATION_IMG3 == \"images/sm_3.gif\";\n",
+ " ANIMATION_IMG4 == \"images/sm_4.gif\";\n",
+ " ANIMATION_IMG5 == \"images/sm_5.gif\";\n",
+ " ANIMATION_IMG6 == \"images/sm_6.gif\";\n",
+ " ANIMATION_IMG7 == \"images/sm_7.gif\";\n",
+ " ANIMATION_IMG8 == \"images/sm_8.gif\";\n",
+ " ANIMATION_IMG9 == \"images/sm_9.gif\"\n",
+ "CONSTANTS Board\n",
+ "PROPERTIES\n",
+ " Board : DOM --> (DOM --> DOM)\n",
+ " ∧\n",
+ " /*@label \"Horizontal and vertical lines\" */\n",
+ " ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2 ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧\n",
+ " Board(y)(x1) ≠ Board(y)(x2))))\n",
+ " /*@desc \"within a vertical or horizontal line all numbers must be different\" */\n",
+ " ∧\n",
+ " \n",
+ " /*@label \"Squares\" */\n",
+ " ∀(s1,s2).(s1:SUBSQ ∧ s2:SUBSQ ⇒\n",
+ " ∀(x1,y1,x2,y2).( (x1∈s1 ∧ x2∈s1 ∧ \n",
+ " x1>=x2 ∧ (x1=x2 ⇒ y1>y2) ∧ // lexicographical ordering\n",
+ " y1∈s2 ∧ y2∈s2 ∧ (x1,y1) ≠ (x2,y2))\n",
+ " ⇒\n",
+ " Board(x1)(y1) ≠ Board(x2)(y2)\n",
+ " ))\n",
+ " /*@desc \"within a sub-square all numbers must be different\" */\n",
+ " ∧\n",
+ " /*@label \"King Moves\" */\n",
+ " ∀(x,y).(x∈D2 ∧ y∈D2 ⇒\n",
+ " (Board(x)(y) ≠ Board(x-1)(y-1) ∧\n",
+ " Board(x)(y-1) ≠ Board(x-1)(y) )\n",
+ " )\n",
+ " ∧\n",
+ " /*@label \"Orthogonals\" */\n",
+ " ∀(x,y).(x∈D1 ∧ y∈DOM ⇒\n",
+ " ( Board(x)(y) ≠ 1+Board(x+1)(y) ∧\n",
+ " 1+Board(x)(y) ≠ Board(x+1)(y) ∧\n",
+ " Board(y)(x) ≠ 1+Board(y)(x+1) ∧\n",
+ " 1+Board(y)(x) ≠ Board(y)(x+1) )\n",
+ " )\n",
+ " /*@desc \"any two orthogonally adjacent cells cannot contain consecutive digits\" */\n",
+ " ∧\n",
+ "\n",
+ " /*@label \"Knight Moves 1\" */\n",
+ " ∀(x,y).(x∈D1 ∧ y∈DOM ⇒\n",
+ " ( y+2∈DOM ⇒ Board(x)(y) ≠ Board(x+1)(y+2) ) ∧\n",
+ " ( y-2∈DOM ⇒ Board(x)(y) ≠ Board(x+1)(y-2) )\n",
+ " ) \n",
+ " ∧\n",
+ " /*@label \"Knight Moves 2\" */\n",
+ " ∀(x,y).(x∈1..7 ∧ y∈DOM ⇒\n",
+ " ( y+1∈DOM ⇒ Board(x)(y) ≠ Board(x+2)(y+1) ) ∧\n",
+ " ( y-1∈DOM ⇒ Board(x)(y) ≠ Board(x+2)(y-1) )\n",
+ " )\n",
+ "\n",
+ " ∧\n",
+ " /* PUZZLE CONSTRAINTS : */\n",
+ " Board(5)(3)=1 ∧ Board(6)(7)=2\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "This corresponds to the solution in https://www.youtube.com/watch?v=yKf9aUIxdb4 \n",
+ "We can see that there is only one solution:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n",
+ " -->\n",
+ "<!-- Title: visited_states Pages: 1 -->\n",
+ "<svg width=\"1162pt\" height=\"394pt\"\n",
+ " viewBox=\"0.00 0.00 1162.00 394.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 390)\">\n",
+ "<title>visited_states</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-390 1159,-390 1159,5 -4,5\"/>\n",
+ "<!-- root -->\n",
+ "<g id=\"node1\" class=\"node\"><title>root</title>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"577,-340.7 622.195,-374.15 531.805,-374.15 577,-340.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"577\" y=\"-359.4\" font-family=\"Times,serif\" font-size=\"12.00\">root</text>\n",
+ "</g>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"1154.21,-217.7 -0.213017,-217.7 -0.213017,-166.3 1154.21,-166.3 1154.21,-217.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"577\" y=\"-202.8\" font-family=\"Times,serif\" font-size=\"12.00\">Board(1) = {(1|->4),(2|->8),(3|->3),(4|->7),(5|->2),(6|->6),(7|->1),(8|->5),(9|-...,Board(2) = {(1|->7),(2|->2),(3|->6),(4|->1),(5|->5),(6|->9),(7|->4),(8|->8),(9|-...,Board(3) = {(1|->1),(2|->5),(3|->9),(4|->4),(5|->8),(6|->3),(7|->7),(8|->2),(9|-...,</text>\n",
+ "<text text-anchor=\"middle\" x=\"577\" y=\"-188.4\" font-family=\"Times,serif\" font-size=\"12.00\">Board(4) = {(1|->8),(2|->3),(3|->7),(4|->2),(5|->6),(6|->1),(7|->5),(8|->9),(9|-...,Board(5) = {(1|->2),(2|->6),(3|->1),(4|->5),(5|->9),(6|->4),(7|->8),(8|->3),(9|-...,Board(6) = {(1|->5),(2|->9),(3|->4),(4|->8),(5|->3),(6|->7),(7|->2),(8|->6),(9|-...,</text>\n",
+ "<text text-anchor=\"middle\" x=\"577\" y=\"-174\" font-family=\"Times,serif\" font-size=\"12.00\">Board(7) = {(1|->3),(2|->7),(3|->2),(4|->6),(5|->1),(6|->5),(7|->9),(8|->4),(9|-...,Board(8) = {(1|->6),(2|->1),(3|->5),(4|->9),(5|->4),(6|->8),(7|->3),(8|->7),(9|-...,Board(9) = {(1|->9),(2|->4),(3|->8),(4|->3),(5|->7),(6|->2),(7|->6),(8|->1),(9|-...</text>\n",
+ "</g>\n",
+ "<!-- root->0 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>root->0</title>\n",
+ "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M577,-340.596C577,-312.305 577,-262.089 577,-228.179\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"580.5,-227.79 577,-217.79 573.5,-227.79 580.5,-227.79\"/>\n",
+ "<text text-anchor=\"middle\" x=\"633.662\" y=\"-275.4\" font-family=\"Times,serif\" font-size=\"12.00\">SETUP_CONSTANTS</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node5\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"604,-14.5442 604,-29.4558 588.184,-40 565.816,-40 550,-29.4558 550,-14.5442 565.816,-4 588.184,-4 604,-14.5442\"/>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"608,-12.4034 608,-31.5966 589.395,-44 564.605,-44 546,-31.5966 546,-12.4034 564.605,-3.55271e-15 589.395,-0 608,-12.4034\"/>\n",
+ "</g>\n",
+ "<!-- 0->1 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>0->1</title>\n",
+ "<path fill=\"none\" stroke=\"#006391\" d=\"M577,-166.211C577,-136.526 577,-86.7671 577,-54.4156\"/>\n",
+ "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"580.5,-54.1656 577,-44.1656 573.5,-54.1657 580.5,-54.1656\"/>\n",
+ "<text text-anchor=\"middle\" x=\"622.976\" y=\"-101.4\" font-family=\"Times,serif\" font-size=\"12.00\">INITIALISATION</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: state_space []>"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot state_space"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/puzzles/images/sm_1.gif b/puzzles/images/sm_1.gif
new file mode 100644
index 0000000000000000000000000000000000000000..d8e44e8a29b28259369b23cd168a4a7693f6b55a
Binary files /dev/null and b/puzzles/images/sm_1.gif differ
diff --git a/puzzles/images/sm_2.gif b/puzzles/images/sm_2.gif
new file mode 100644
index 0000000000000000000000000000000000000000..ac3bee6afea292ec9a57b4f81d95b5879779d832
Binary files /dev/null and b/puzzles/images/sm_2.gif differ
diff --git a/puzzles/images/sm_3.gif b/puzzles/images/sm_3.gif
new file mode 100644
index 0000000000000000000000000000000000000000..b1fd71fd60c640380aefc040e373602b8b310366
Binary files /dev/null and b/puzzles/images/sm_3.gif differ
diff --git a/puzzles/images/sm_4.gif b/puzzles/images/sm_4.gif
new file mode 100644
index 0000000000000000000000000000000000000000..09928bb2535a7e56a2cf7153c6693a1e009d7935
Binary files /dev/null and b/puzzles/images/sm_4.gif differ
diff --git a/puzzles/images/sm_5.gif b/puzzles/images/sm_5.gif
new file mode 100644
index 0000000000000000000000000000000000000000..2eda94e9e98c215f68bea26bd8b9d5ce089ff87f
Binary files /dev/null and b/puzzles/images/sm_5.gif differ
diff --git a/puzzles/images/sm_6.gif b/puzzles/images/sm_6.gif
new file mode 100644
index 0000000000000000000000000000000000000000..f46bafd01cb88856a3a14d5ad833a22a2096a7e5
Binary files /dev/null and b/puzzles/images/sm_6.gif differ
diff --git a/puzzles/images/sm_7.gif b/puzzles/images/sm_7.gif
new file mode 100644
index 0000000000000000000000000000000000000000..de46e4aae533aa301be7fc937d392e34aead3e76
Binary files /dev/null and b/puzzles/images/sm_7.gif differ
diff --git a/puzzles/images/sm_8.gif b/puzzles/images/sm_8.gif
new file mode 100644
index 0000000000000000000000000000000000000000..b97c3d1ec05287b6af5e0071ed093cc078057f14
Binary files /dev/null and b/puzzles/images/sm_8.gif differ
diff --git a/puzzles/images/sm_9.gif b/puzzles/images/sm_9.gif
new file mode 100644
index 0000000000000000000000000000000000000000..bee8858cafe62a317ca60af798cb54864cf80b2e
Binary files /dev/null and b/puzzles/images/sm_9.gif differ