From a35f55de54d044c759b074b440e686dddc67ff2c Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Fri, 11 May 2018 12:32:00 +0200
Subject: [PATCH] add more puzzles to notebook

---
 notebooks/tutorials/prob_solver_intro.ipynb | 132 ++++++++++++++++++++
 1 file changed, 132 insertions(+)

diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 3a7c066..cf804ae 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -395,6 +395,138 @@
     "        (B=TRUE <=> A=TRUE) }"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Sudoku\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE (DOM = (1 ‥ 9) ∧ Board = {(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(5↦3),(6↦2),(7↦9),(8↦4),(9↦5)}),(2↦{(1↦9),(2↦5),(3↦2),(4↦7),(5↦1),(6↦4),(7↦6),(8↦3),(9↦8)}),(3↦{(1↦4),(2↦3),(3↦6),(4↦8),(5↦9),(6↦5),(7↦7),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(5↦7),(6↦6),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(5↦8),(6↦1),(7↦2),(8↦9),(9↦4)}),(6↦{(1↦5),(2↦1),(3↦8),(4↦4),(5↦2),(6↦9),(7↦3),(8↦6),(9↦7)}),(7↦{(1↦1),(2↦9),(3↦4),(4↦2),(5↦6),(6↦7),(7↦5),(8↦8),(9↦3)}),(8↦{(1↦8),(2↦6),(3↦7),(4↦1),(5↦5),(6↦3),(7↦4),(8↦2),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(4↦9),(5↦4),(6↦8),(7↦1),(8↦7),(9↦6)})} ∧ SUBSQ = {{1,2,3},{4,5,6},{7,8,9}})"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    " DOM = 1..9 & \n",
+    " SUBSQ = { {1,2,3}, {4,5,6}, {7,8,9} } &\n",
+    " Board : DOM --> (DOM --> DOM)   &\n",
+    "  !y.(y:DOM => !(x1,x2).(x1:DOM & x1<x2 & x2:DOM  => (Board(x1)(y) /= Board(x2)(y) &\n",
+    "                                                      Board(y)(x1) /= Board(y)(x2)))) &\n",
+    "  !(s1,s2).(s1:SUBSQ & s2:SUBSQ =>\n",
+    "             !(x1,y1,x2,y2).( (x1:s1 & x2:s1 & x1>=x2 & (x1=x2 => y1>y2) &\n",
+    "                               y1:s2 & y2:s2 & (x1,y1) /= (x2,y2))\n",
+    "                              =>\n",
+    "                              Board(x1)(y1) /= Board(x2)(y2)\n",
+    "                            ))\n",
+    "                            \n",
+    "   & /* PUZZLE CONSTRAINTS : */\n",
+    "   \n",
+    "   Board(1)(1)=7 & Board(1)(2)=8  & Board(1)(3)=1 & Board(1)(4)=6 & Board(1)(6)=2 \n",
+    "                 & Board(1)(7)=9 & Board(1)(9) = 5 &\n",
+    "   Board(2)(1)=9 & Board(2)(3)=2 & Board(2)(4)=7 & Board(2)(5)=1 &\n",
+    "   Board(3)(3)=6 & Board(3)(4)=8 & Board(3)(8)=1 & Board(3)(9)=2 &\n",
+    "   \n",
+    "   Board(4)(1)=2 & Board(4)(4)=3 & Board(4)(7)=8 & Board(4)(8)=5 & Board(4)(9)=1 &\n",
+    "   Board(5)(2)=7 & Board(5)(3)=3 & Board(5)(4)=5 & Board(5)(9)=4 &\n",
+    "   Board(6)(3)=8 & Board(6)(6)=9 & Board(6)(7)=3 & Board(6)(8)=6 &\n",
+    "   \n",
+    "   Board(7)(1)=1 & Board(7)(2)=9 & Board(7)(6)=7 & Board(7)(8)=8 &\n",
+    "   Board(8)(1)=8 & Board(8)(2)=6 & Board(8)(3)=7 & Board(8)(6)=3 & Board(8)(7)=4 & Board(8)(9)=9 &\n",
+    "   Board(9)(3)=5 & Board(9)(7)=1"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Subset Sum Puzzle\n",
+    " From Katta G. Murty: \"Optimization Models for Decision Making\", page 340\n",
+    "  http://ioe.engin.umich.edu/people/fac/books/murty/opti_model/junior-7.pdf\n",
+    "  \n",
+    "Example 7.8.1\n",
+    "``A bank van had several bags of coins, each containing either\n",
+    "  16, 17, 23, 24, 39, or 40 coins. While the van was parked on the\n",
+    "  street, thieves stole some bags. A total of 100 coins were lost.\n",
+    "  It is required to find how many bags were stolen.''"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE (stolen = {(16↦2),(17↦4),(23↦0),(24↦0),(39↦0),(40↦0)} ∧ coins = {16,17,23,24,39,40})"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "coins = {16,17,23,24,39,40} &  /* number of coins in each bag */\n",
+    " stolen : coins --> NATURAL & /* number of bags of each type stolen */\n",
+    " SIGMA(x).(x:coins|stolen(x)*x)=100"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Who killed Agatha Puzzle"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE (Persons = {\"Agatha\",\"Charles\",\"butler\"} ∧ richer = {(\"Agatha\"↦\"Charles\"),(\"butler\"↦\"Agatha\"),(\"butler\"↦\"Charles\")} ∧ victim = \"Agatha\" ∧ killer = \"Agatha\" ∧ hates = {(\"Agatha\"↦\"Agatha\"),(\"Agatha\"↦\"Charles\"),(\"Charles\"↦\"butler\"),(\"butler\"↦\"Agatha\"),(\"butler\"↦\"Charles\")})"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "Persons = { \"Agatha\", \"butler\", \"Charles\"} /* it is more efficient in B to use enumerated sets; but in the eval window we cannot define them */\n",
+    " &\n",
+    " hates : Persons <-> Persons &\n",
+    " richer : Persons <-> Persons &  /* richer /\\ richer~ = {} & */\n",
+    " richer /\\ id(Persons) = {} &\n",
+    " !(x,y,z).(x|->y:richer & y|->z:richer => x|->z:richer) &\n",
+    " !(x,y).(x:Persons & y:Persons & x/=y => (x|->y:richer <=> y|->x /: richer)) &\n",
+    " \n",
+    " killer : Persons &   victim : Persons &\n",
+    " killer|->victim : hates & /* A killer always hates his victim */\n",
+    " killer|->victim /: richer & /* and is no richer than his victim */\n",
+    " hates[{ \"Agatha\"}] /\\ hates[{\"Charles\"}] = {} & /* Charles hates noone that Agatha hates. */\n",
+    " hates[{ \"Agatha\"}] = Persons - {\"butler\"} & /* Agatha hates everybody except the butler. */\n",
+    " !x.( x: Persons & x|-> \"Agatha\" /: richer => \"butler\"|->x : hates) & /* The butler hates everyone not richer than Aunt Agatha */\n",
+    " hates[{ \"Agatha\"}] <: hates[{\"butler\"}] & /* The butler hates everyone whom Agatha hates.  */\n",
+    " !x.(x:Persons => hates[{x}] /= Persons) /* Noone hates everyone. */ &\n",
+    " victim =  \"Agatha\""
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
-- 
GitLab