From 1e2d3db5e3dbd0491a61ae6d2951be45ab48e4d0 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 21 May 2020 11:21:09 +0200
Subject: [PATCH] add miracle Sudoku example
---
puzzles/Sudoku_Miracle.ipynb | 1025 ++++++++++++++++++++++++++++++++++
puzzles/images/sm_1.gif | Bin 0 -> 174 bytes
puzzles/images/sm_2.gif | Bin 0 -> 250 bytes
puzzles/images/sm_3.gif | Bin 0 -> 253 bytes
puzzles/images/sm_4.gif | Bin 0 -> 252 bytes
puzzles/images/sm_5.gif | Bin 0 -> 249 bytes
puzzles/images/sm_6.gif | Bin 0 -> 256 bytes
puzzles/images/sm_7.gif | Bin 0 -> 235 bytes
puzzles/images/sm_8.gif | Bin 0 -> 261 bytes
puzzles/images/sm_9.gif | Bin 0 -> 258 bytes
10 files changed, 1025 insertions(+)
create mode 100644 puzzles/Sudoku_Miracle.ipynb
create mode 100644 puzzles/images/sm_1.gif
create mode 100644 puzzles/images/sm_2.gif
create mode 100644 puzzles/images/sm_3.gif
create mode 100644 puzzles/images/sm_4.gif
create mode 100644 puzzles/images/sm_5.gif
create mode 100644 puzzles/images/sm_6.gif
create mode 100644 puzzles/images/sm_7.gif
create mode 100644 puzzles/images/sm_8.gif
create mode 100644 puzzles/images/sm_9.gif
diff --git a/puzzles/Sudoku_Miracle.ipynb b/puzzles/Sudoku_Miracle.ipynb
new file mode 100644
index 0000000..751a788
--- /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
GIT binary patch
literal 174
zcmZ?wbhEHb)Mn6T_`qQJ|Nnmm1_m7l1_lO@2m@1ZOaIE#GW?6@Z1EDFbx)W1eCr(c
zu4hj3R!v&>u6=Kw_WTmvd(WmG*OtH3t7d)w*e8ucZDOe_n@iXh?|nK^%H&;xa&BMs
z7eD17(T%@koKKl;a61vRxc*(A#k@JQU-$i<y5>6DjMS~BH$s1uN=#cZ&3#6j_|5AY
fC)=1iD_8z}c6=tocg|OuubNA`q5`vm7#OSpB#BSk
literal 0
HcmV?d00001
diff --git a/puzzles/images/sm_2.gif b/puzzles/images/sm_2.gif
new file mode 100644
index 0000000000000000000000000000000000000000..ac3bee6afea292ec9a57b4f81d95b5879779d832
GIT binary patch
literal 250
zcmZ?wbhEHb)Mn6T_{?DV|NsBp98Apq!VJU#9gs4RUIv!+0w+9I@0HkpcK82;7oPrU
z^CCG{WOT1uqaFVtC;IE!^-tD4-zO=csv*^VNbchamu+n`mW6x>Nn3VF>wL@Ec?(4K
z9p-F`o0a(NbdF>29kmb9w)X3`TUAKrD`(%(tE;bRY%*z357sLRZ)-N}?CWo>ikc8O
zsd{?u%vs(g<~_o53p+|<-O6V#Ua??a@7k5|%Y-(TZEnfj7P4ct<NE#GTMk+rJ|eQ{
T_=#huqLt2HxNz23kii-NqKsiQ
literal 0
HcmV?d00001
diff --git a/puzzles/images/sm_3.gif b/puzzles/images/sm_3.gif
new file mode 100644
index 0000000000000000000000000000000000000000..b1fd71fd60c640380aefc040e373602b8b310366
GIT binary patch
literal 253
zcmZ?wbhEHb)Mn6T_{?DV|NsBp98Apq!fL8h8HfNnAT=Pp3@n=jPI#`~E3yCV?*9od
zJpI$=MRKml=w7u(JN`pX^w+iPpR9YnPg1~CLyCP{;<FPvr>0C_c7=7V$MUsWPrGb0
zRd1|&$(@lm^X5GvTf_ZVB+O^LZN2>@c{k7e=Wo}CRH-*K*6Fomw&}*S8oG3pb{W@5
zHKn^xckAp6D@mQFIW2eI6q7~8B}*-quZWqIKS^xejM@F0d%M^9ubH`J_eRHwa}L%X
aJ~H*d@nt7ZiKd**Qo3~c@&#i-25SK8>SY7~
literal 0
HcmV?d00001
diff --git a/puzzles/images/sm_4.gif b/puzzles/images/sm_4.gif
new file mode 100644
index 0000000000000000000000000000000000000000..09928bb2535a7e56a2cf7153c6693a1e009d7935
GIT binary patch
literal 252
zcmZ?wbhEHb)Mn6T_{?DV|NsBp98Apq!fL8h8HfNnAT=Pp3@jT3PI#`~E3yCV?*9od
zJpI$=MRKml=w7u(JN`pX^w+iPpR9YnPtxFp)GnqIDGP4Q)|~1y?{jC*v4AT}N@v}b
z+kAD}MHasOvu=C}>QQrEdGE3?L%R3fs9$&L_P%+YUM^8x6;M;u)>_$EE7H=Hrk>oF
z)u5RxHg%fR4AEKrbDCz(@1DMB-jaz6dow#H&DEW~Y)!{HwaIIjZr`wT)n*r`JqJt<
a9Twej?D)}>zFW?mRl0cT;&~%M25SHvS7@&Q
literal 0
HcmV?d00001
diff --git a/puzzles/images/sm_5.gif b/puzzles/images/sm_5.gif
new file mode 100644
index 0000000000000000000000000000000000000000..2eda94e9e98c215f68bea26bd8b9d5ce089ff87f
GIT binary patch
literal 249
zcmZ?wbhEHb)Mn6T_{?DV|NsBp98Apq!fL8h|M#*m5CS?N1t7f)Eb9bLc&^?nvH$Gu
z{|PTV{nO?}a<0heUbRL${zFdm*R|`Ptb4vs(%^+u8pnwxK|fzDoOU5)a(P$Oa>E|e
zuG+lmceN_g_c+w1o|f2Pw^aK<?u{?Dv+qr*n*D6a>zSIh?qxYGH6e8k!fh5!Rz0E>
zdJ{w@3H3}7p4Qqmy?SC_TJ=o7$VJ&PjUAm;c?*}XEnmN(Xx-|ht=pFEn7hlxY4iT}
Z-G>ez)t!C(<WU2qbLY<;Hxp#A1^|7%W+4Co
literal 0
HcmV?d00001
diff --git a/puzzles/images/sm_6.gif b/puzzles/images/sm_6.gif
new file mode 100644
index 0000000000000000000000000000000000000000..f46bafd01cb88856a3a14d5ad833a22a2096a7e5
GIT binary patch
literal 256
zcmZ?wbhEHb)Mn6T_{?DV|NsBp98Apq!fL8h|M#-gU2b8(3v@uTAiWGMTLn&duHGxL
z|LpGn2`@bT)8<8TuE^+KwMIMsLr(P9wd<d(d%jQdLa2rm_ojz0Pv~r$GIQCNtInRw
z)n7dA@(rEt?q&SD*XU^a<ZVXx)?Q33m%Qv3T$!-$qvicqkF#pU>Ko!J)LL3insQ2W
z+YC#}82Y7p3aW*tcDJXs&bF97Yw`lo{KfMp&zU%>Fm~G9dG+OM>RPtAY~HamTyOcd
juEvdyyN~Q!bZps)lfwJYgl;{5N?YmbwX2tm1sSXXKznRn
literal 0
HcmV?d00001
diff --git a/puzzles/images/sm_7.gif b/puzzles/images/sm_7.gif
new file mode 100644
index 0000000000000000000000000000000000000000..de46e4aae533aa301be7fc937d392e34aead3e76
GIT binary patch
literal 235
zcmZ?wbhEHb)Mn6T_{?DV|NsBp98Apq!fL8h|M#-gU2d5tx{d)i&;dz-^fIt45IEtv
zdauO(v%CK%yzul-n-|HsBBOiN8twQGIniI&u79%b`94X57gA9?Czcd-)_gTOv*Oap
zX0N4JZhVwFJ8Q??$$`gmdZQCRUJf%`e=_&Ij&8et>ht%q|J^RW&Zw>lZESL_t!m3_
zsq5;F3hQg=3^uEbo|M%y#nXJcNPYWkiG}^GQ>S%^FP-c%Yr;CsRU1t<ZxNlp-G9R_
Q5d)<I2M_Eu5@fIj0Dc)^aR2}S
literal 0
HcmV?d00001
diff --git a/puzzles/images/sm_8.gif b/puzzles/images/sm_8.gif
new file mode 100644
index 0000000000000000000000000000000000000000..b97c3d1ec05287b6af5e0071ed093cc078057f14
GIT binary patch
literal 261
zcmZ?wbhEHb)Mn6T_{?DV|NsBp98Apq!fL8h|M#-gU2d5tx~}fPDFz%s2P6*C%fPZr
z;DqPuy%PJ+?*5<f!qY!(UL@y=jP6xywBtYIM1Nho{>i%M`y>TQHKe)^$$dQGvaM~#
zvM(P(W-U9b_5Re76#szJ;YNOui|=|y7Vn#Keakir-(|D6-${=BKWX<yw<tsP2&2UM
z2EBICva<5#;+pElgu1xizQT%(Nel%R)3RpF&6(XXWwM`I_oB?8+GP_PR`h#s4%ska
vQ|C_I?Oh9ZZ`teUx$)@ggC|7SoIZ2voY$_4=Z{|zF;Kd7`_^?MK?Z98Q6q9_
literal 0
HcmV?d00001
diff --git a/puzzles/images/sm_9.gif b/puzzles/images/sm_9.gif
new file mode 100644
index 0000000000000000000000000000000000000000..bee8858cafe62a317ca60af798cb54864cf80b2e
GIT binary patch
literal 258
zcmZ?wbhEHb)Mn6T_{?DV|NsBp98Apq!fL8h|M#-gU2d5tx~}fPsg8~g25dkFBnZ;W
zz_MN7gy-tL68q2Y{-5x|(?4xqB<G5Z?p15F<3Hp?e_gx&$-3wJBsa8bNC_U2`*^}-
zTieWKUsjrUu3w+^<<^-`ezBf6Shn^YJrlgMh;2*ZE$`p4k-^V0i|)*se?haXt~SFx
zt2!q+xGFw6re3(Qsjs!$P-1ekNqbFfzt^;|Df8kN7%!fvv3&L<w~n=KJ=15-oVBrN
v#`>u%cZ6)))Tg(iyzAg<N2z1S3-+DTJb8A)`3p-f$0=REapS77AcHjku>5lq
literal 0
HcmV?d00001
--
GitLab