add golomb ruler and graph iso

d488cbd4 · Michael Leuschel · 95b79dab · d488cbd4
Commit d488cbd4 authored 7 years ago by Michael Leuschel
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -13,7 +13,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 1,
+   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
@@ -22,7 +22,7 @@
       "1024"
      ]
     },
-     "execution_count": 1,
+     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -588,12 +588,89 @@
    " victim =  \"Agatha\""
   ]
  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Golomb Ruler\n",
+    "A Golomb ruler with $n$ marks of length $len$ has the property that all distances between distinct marks are different\n",
+    "The following expresses the problem in B:"
+   ]
+  },
  {
   "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 1,
   "metadata": {},
-   "outputs": [],
-   "source": []
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\ta = {(1↦0),(2↦2),(3↦6),(4↦9),(5↦14),(6↦24),(7↦25)}\n",
+       "\tlen = 25\n",
+       "\tn = 7"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "n=7 & len=25 &\n",
+    "a:1..n --> 0..len & !i.(i:2..n => a(i-1) < a(i)) & \n",
+    "!(i1,j1,i2,j2).(( i1>0 & i2>0 & j1<=n & j2 <= n & i1<j1 & i2<j2 & (i1,j1) /= (i2,j2)) => (a(j1)-a(i1) /= a(j2)-a(i2)))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Graph Isomorphism\n",
+    "We can check two graphs $g1$ and $g2$ for isomporhism by trying to find a solution for the following predicate:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tn1 = \"a\"\n",
+       "\tiso = {(1↦\"c\"),(2↦\"a\"),(3↦\"b\")}\n",
+       "\tn2 = \"b\"\n",
+       "\tn3 = \"c\"\n",
+       "\tV = {1,2,3}\n",
+       "\tg1 = {(1↦2),(1↦3),(2↦3)}\n",
+       "\tg2 = {(\"a\"↦\"b\"),(\"c\"↦\"a\"),(\"c\"↦\"b\")}\n",
+       "\tv1 = 1\n",
+       "\tv2 = 2\n",
+       "\tv3 = 3\n",
+       "\tN = {\"a\",\"b\",\"c\"}"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "LET V,N,v1,v2,v3,n1,n2,n3 BE\n",
+    "  v1=1 & v2=2 & v3=3 & n1=\"a\" & n2=\"b\" & n3=\"c\" &\n",
+    "  V = {v1,v2,v3} & N = {n1,n2,n3}\n",
+    "IN\n",
+    "g1 = {v1 |->v2, v1|->v3, v2|->v3} &\n",
+    "g2 = {n3 |->n2, n3|->n1, n1|->n2} &\n",
+    "iso: V >->> N & !v.(v:V => iso[g1[{v}]] = g2[iso[{v}]])\n",
+    "END"
+   ]
  },
  {
   "cell_type": "code",

 %% Cell type:markdown id: tags:

 # Introduction to ProB's constraint solving capabilities
 We can use ProB to perform computations:

 ## Expressions
 Expressions in B have a value. With ProB and with ProB's Jupyter backend, you can evaluate expresssions such as:

 %% Cell type:code id: tags:

 ``` prob
 2**10
 ```

 %% Output

    1024

 %% Cell type:markdown id: tags:

 ProB supports *mathematical* integers without restriction (apart from memmory consumption):

 %% Cell type:code id: tags:

 ``` prob
 2**100
 ```

 %% Output

    1267650600228229401496703205376

 %% Cell type:markdown id: tags:

 ## Predicates
 ProB can also be used to evaluate predicates (B distinguishes between expressions which have a value and predicates which are either true or false).

 %% Cell type:code id: tags:

 ``` prob
 2+2>3
 ```

 %% Output

    TRUE

 %% Cell type:markdown id: tags:

 Within predicates you can use **open** variables, which are implicitly existentially quantified.
 ProB will display the solution for the open variables, if possible.

 %% Cell type:code id: tags:

 ``` prob
 x*x=100
 ```

 %% Output

    TRUE
    
    Solution:
    	x = −10

 %% Cell type:markdown id: tags:

 We can find all solutions to a predicate by using the set comprehension notation.
 Note that by this we turn a predicate into an expression.

 %% Cell type:code id: tags:

 ``` prob
 {x|x*x=100}
 ```

 %% Output

    {−10,10}

 %% Cell type:markdown id: tags:

 ## Send More Money Puzzle
 We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:

 %% Cell type:code id: tags:

 ``` prob
  {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
   card({S,E,N,D, M,O,R, Y}) = 8 &
   S*1000 + E*100 + N*10 + D +
   M*1000 + O*100 + R*10 + E =
  M*10000 + O*1000 + N*100 + E*10 + Y
 ```

 %% Output

    TRUE
    
    Solution:
    	R = 8
    	S = 9
    	D = 7
    	E = 5
    	Y = 2
    	M = 1
    	N = 6
    	O = 0

 %% Cell type:markdown id: tags:

 Observe how we have used the cardinality constraint to express that all digits are distinct.
 If we leave out this cardinality constraint, other solutions are possible:

 %% Cell type:code id: tags:

 ``` prob
  {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
  // card({S,E,N,D, M,O,R, Y}) = 8 & // commented out
   S*1000 + E*100 + N*10 + D +
   M*1000 + O*100 + R*10 + E =
  M*10000 + O*1000 + N*100 + E*10 + Y
 ```

 %% Output

    TRUE
    
    Solution:
    	R = 0
    	S = 9
    	D = 0
    	E = 0
    	Y = 0
    	M = 1
    	N = 0
    	O = 0

 %% Cell type:markdown id: tags:

 We can find all solutions (to the unmodified puzzle) using a set comprehension and make sure that there is just a single soltuion:

 %% Cell type:code id: tags:

 ``` prob
  {S,E,N,D, M,O,R, Y |
   {S,E,N,D, M,O,R, Y} <: 0..9 &  S >0 & M >0 &
   card({S,E,N,D, M,O,R, Y}) = 8 &
   S*1000 + E*100 + N*10 + D +
   M*1000 + O*100 + R*10 + E =
   M*10000 + O*1000 + N*100 + E*10 + Y }
 ```

 %% Output

    {(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}

 %% Cell type:markdown id: tags:

 ## KISS PASSION Puzzle
 A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem.

 %% Cell type:code id: tags:

 ``` prob
    {K,P} <: 1..9 &
    {I,S,A,O,N} <: 0..9 &
    (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S)
     =  1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &
    card({K, I, S, P, A, O, N}) = 7
 ```

 %% Output

    TRUE
    
    Solution:
    	P = 4
    	A = 1
    	S = 3
    	I = 0
    	K = 2
    	N = 9
    	O = 8

 %% Cell type:markdown id: tags:

 ## N-Queens Puzzle
 Here is how we can solve the famous N-Queens puzzle for n=8.

 %% Cell type:code id: tags:

 ``` prob
 n = 8 &
 queens : perm(1..n) /* for each column the row in which the queen is in */
 &
 !(q1,q2).(q1:1..n & q2:2..n & q2>q1
    => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))
 ```

 %% Output

    TRUE
    
    Solution:
    	queens = {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)}
    	n = 8

 %% Cell type:code id: tags:

 ``` prob
 n = 16 &
 queens : perm(1..n) /* for each column the row in which the queen is in */
 &
 !(q1,q2).(q1:1..n & q2:2..n & q2>q1
    => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))
 ```

 %% Output

    TRUE
    
    Solution:
    	queens = {(1↦1),(2↦3),(3↦5),(4↦13),(5↦11),(6↦4),(7↦15),(8↦7),(9↦16),(10↦14),(11↦2),(12↦8),(13↦6),(14↦9),(15↦12),(16↦10)}
    	n = 16

 %% Cell type:markdown id: tags:

 ## Knights and Knave Puzzle
 Here is a puzzle from Smullyan involving an island with only knights and knaves.
 We know that:
 - Knights: always tell the truth
 - Knaves: always lie

 We are given the following information about three persons A,B,C on the island:
 1. A says: “B is a knave or C is a knave”
 2. B says “A is a knight”

 What are A, B and C?
 Note: we model A,B,C as boolean variables which are equal to TRUE if they are a knight and FALSE if they are a knave.

 %% Cell type:code id: tags:

 ``` prob
 (A=TRUE <=> (B=FALSE or C=FALSE)) & // Sentence 1
 (B=TRUE <=> A=TRUE) // Sentence 2
 ```

 %% Output

    TRUE
    
    Solution:
    	A = TRUE
    	B = TRUE
    	C = FALSE

 %% Cell type:markdown id: tags:

 Note that in B there are no propositional variables: A,B and C are expressions with a value.
 To turn them into a predicate we need to use the comparison with TRUE.

 %% Cell type:code id: tags:

 ``` prob
 /* this computes the set of all models: */
 {A,B,C| (A=TRUE <=> (B=FALSE or C=FALSE)) &
        (B=TRUE <=> A=TRUE) }
 ```

 %% Output

    {((TRUE↦TRUE)↦FALSE)}

 %% Cell type:markdown id: tags:

 ## Sudoku

 %% Cell type:code id: tags:

 ``` prob
 DOM = 1..9 &
 SUBSQ = { {1,2,3}, {4,5,6}, {7,8,9} } &
 Board : DOM --> (DOM --> DOM)   &
  !y.(y:DOM => !(x1,x2).(x1:DOM & x1<x2 & x2:DOM  => (Board(x1)(y) /= Board(x2)(y) &
                                                      Board(y)(x1) /= Board(y)(x2)))) &
  !(s1,s2).(s1:SUBSQ & s2:SUBSQ =>
             !(x1,y1,x2,y2).( (x1:s1 & x2:s1 & x1>=x2 & (x1=x2 => y1>y2) &
                               y1:s2 & y2:s2 & (x1,y1) /= (x2,y2))
                              =>
                              Board(x1)(y1) /= Board(x2)(y2)
                            ))

   & /* PUZZLE CONSTRAINTS : */

   Board(1)(1)=7 & Board(1)(2)=8  & Board(1)(3)=1 & Board(1)(4)=6 & Board(1)(6)=2
                 & Board(1)(7)=9 & Board(1)(9) = 5 &
   Board(2)(1)=9 & Board(2)(3)=2 & Board(2)(4)=7 & Board(2)(5)=1 &
   Board(3)(3)=6 & Board(3)(4)=8 & Board(3)(8)=1 & Board(3)(9)=2 &

   Board(4)(1)=2 & Board(4)(4)=3 & Board(4)(7)=8 & Board(4)(8)=5 & Board(4)(9)=1 &
   Board(5)(2)=7 & Board(5)(3)=3 & Board(5)(4)=5 & Board(5)(9)=4 &
   Board(6)(3)=8 & Board(6)(6)=9 & Board(6)(7)=3 & Board(6)(8)=6 &

   Board(7)(1)=1 & Board(7)(2)=9 & Board(7)(6)=7 & Board(7)(8)=8 &
   Board(8)(1)=8 & Board(8)(2)=6 & Board(8)(3)=7 & Board(8)(6)=3 & Board(8)(7)=4 & Board(8)(9)=9 &
   Board(9)(3)=5 & Board(9)(7)=1
 ```

 %% Output

    TRUE
    
    Solution:
    	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}}

 %% Cell type:markdown id: tags:

 ## Subset Sum Puzzle
 From Katta G. Murty: "Optimization Models for Decision Making", page 340
  http://ioe.engin.umich.edu/people/fac/books/murty/opti_model/junior-7.pdf

 Example 7.8.1
 ``A bank van had several bags of coins, each containing either
  16, 17, 23, 24, 39, or 40 coins. While the van was parked on the
  street, thieves stole some bags. A total of 100 coins were lost.
  It is required to find how many bags were stolen.''

 %% Cell type:code id: tags:

 ``` prob
 coins = {16,17,23,24,39,40} &  /* number of coins in each bag */
 stolen : coins --> NATURAL & /* number of bags of each type stolen */
 SIGMA(x).(x:coins|stolen(x)*x)=100
 ```

 %% Output

    TRUE
    
    Solution:
    	stolen = {(16↦2),(17↦4),(23↦0),(24↦0),(39↦0),(40↦0)}
    	coins = {16,17,23,24,39,40}

 %% Cell type:markdown id: tags:

 ## Who killed Agatha Puzzle

 %% Cell type:code id: tags:

 ``` prob
 Persons = { "Agatha", "butler", "Charles"} /* it is more efficient in B to use enumerated sets; but in the eval window we cannot define them */
 &
 hates : Persons <-> Persons &
 richer : Persons <-> Persons &  /* richer /\ richer~ = {} & */
 richer /\ id(Persons) = {} &
 !(x,y,z).(x|->y:richer & y|->z:richer => x|->z:richer) &
 !(x,y).(x:Persons & y:Persons & x/=y => (x|->y:richer <=> y|->x /: richer)) &

 killer : Persons &   victim : Persons &
 killer|->victim : hates & /* A killer always hates his victim */
 killer|->victim /: richer & /* and is no richer than his victim */
 hates[{ "Agatha"}] /\ hates[{"Charles"}] = {} & /* Charles hates noone that Agatha hates. */
 hates[{ "Agatha"}] = Persons - {"butler"} & /* Agatha hates everybody except the butler. */
 !x.( x: Persons & x|-> "Agatha" /: richer => "butler"|->x : hates) & /* The butler hates everyone not richer than Aunt Agatha */
 hates[{ "Agatha"}] <: hates[{"butler"}] & /* The butler hates everyone whom Agatha hates.  */
 !x.(x:Persons => hates[{x}] /= Persons) /* Noone hates everyone. */ &
 victim =  "Agatha"
 ```

 %% Output

    TRUE
    
    Solution:
    	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")}

+%% Cell type:markdown id: tags:
+
+## Golomb Ruler
+A Golomb ruler with $n$ marks of length $len$ has the property that all distances between distinct marks are different
+The following expresses the problem in B:
+
 %% Cell type:code id: tags:

 ``` prob
+n=7 & len=25 &
+a:1..n --> 0..len & !i.(i:2..n => a(i-1) < a(i)) &
+!(i1,j1,i2,j2).(( i1>0 & i2>0 & j1<=n & j2 <= n & i1<j1 & i2<j2 & (i1,j1) /= (i2,j2)) => (a(j1)-a(i1) /= a(j2)-a(i2)))
 ```

+%% Output
+
+    TRUE
+    
+    Solution:
+    	a = {(1↦0),(2↦2),(3↦6),(4↦9),(5↦14),(6↦24),(7↦25)}
+    	len = 25
+    	n = 7
+
+%% Cell type:markdown id: tags:
+
+## Graph Isomorphism
+We can check two graphs $g1$ and $g2$ for isomporhism by trying to find a solution for the following predicate:
+
+%% Cell type:code id: tags:
+
+``` prob
+LET V,N,v1,v2,v3,n1,n2,n3 BE
+  v1=1 & v2=2 & v3=3 & n1="a" & n2="b" & n3="c" &
+  V = {v1,v2,v3} & N = {n1,n2,n3}
+IN
+g1 = {v1 |->v2, v1|->v3, v2|->v3} &
+g2 = {n3 |->n2, n3|->n1, n1|->n2} &
+iso: V >->> N & !v.(v:V => iso[g1[{v}]] = g2[iso[{v}]])
+END
+```
+
+%% Output
+
+    TRUE
+    
+    Solution:
+    	n1 = "a"
+    	iso = {(1↦"c"),(2↦"a"),(3↦"b")}
+    	n2 = "b"
+    	n3 = "c"
+    	V = {1,2,3}
+    	g1 = {(1↦2),(1↦3),(2↦3)}
+    	g2 = {("a"↦"b"),("c"↦"a"),("c"↦"b")}
+    	v1 = 1
+    	v2 = 2
+    	v3 = 3
+    	N = {"a","b","c"}
+
 %% Cell type:code id: tags:

 ``` prob
 ```