diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 3a7c066e85a02b1cbc88856dfa12f6b22c2c813b..cf804ae1788493c923a32f1813b4888873c8e9ee 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,