Skip to content
Snippets Groups Projects
Commit 7b04452b authored by Michael Leuschel's avatar Michael Leuschel
Browse files

update notebook

parent 267b3908
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/tutorials/prob_solver_intro.ipynb
+ 212
− 21
View file @ 7b04452b
%% 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
2**102
```
%% Output
1024
$5070602400912917605986812821504$
5070602400912917605986812821504
%% 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$
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$
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$
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\}$
{−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$
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$
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\mapsto 5)\mapsto 6)\mapsto 7)\mapsto 1)\mapsto 0)\mapsto 8)\mapsto 2)\}$
{(((((((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$
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\mapsto 1),(2\mapsto 5),(3\mapsto 8),(4\mapsto 6),(5\mapsto 3),(6\mapsto 7),(7\mapsto 2),(8\mapsto 4)\}$
* $n = 8$
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
:table {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)}
```
%% Output
|Nr|prj1|prj2|
|---|---|---|
|1|1|1|
|2|2|5|
|3|3|8|
|4|4|6|
|5|5|3|
|6|6|7|
|7|7|2|
|8|8|4|
Nr prj1 prj2
1 1 1
2 2 5
3 3 8
4 4 6
5 5 3
6 6 7
7 7 2
8 8 4
%% 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\mapsto 1),(2\mapsto 3),(3\mapsto 5),(4\mapsto 13),(5\mapsto 11),(6\mapsto 4),(7\mapsto 15),(8\mapsto 7),(9\mapsto 16),(10\mapsto 14),(11\mapsto 2),(12\mapsto 8),(13\mapsto 6),(14\mapsto 9),(15\mapsto 12),(16\mapsto 10)\}$
* $n = 16$
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$
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\mapsto TRUE)\mapsto FALSE)\}$
{((TRUE↦TRUE)↦FALSE)}
%% Cell type:code id: tags:
``` prob
:table {A,B,C| (A=TRUE <=> (B=FALSE or C=FALSE)) &
(B=TRUE <=> A=TRUE) }
```
%% Output
|Nr|A|B|C|
|---|---|---|---|
|1|TRUE|TRUE|FALSE|
Nr A B C
1 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 \ldots 9)$
* $Board = \{(1\mapsto\{(1\mapsto 7),(2\mapsto 8),(3\mapsto 1),(4\mapsto 6),(5\mapsto 3),(6\mapsto 2),(7\mapsto 9),(8\mapsto 4),(9\mapsto 5)\}),(2\mapsto\{(1\mapsto 9),(2\mapsto 5),(3\mapsto 2),(4\mapsto 7),(5\mapsto 1),(6\mapsto 4),(7\mapsto 6),(8\mapsto 3),(9\mapsto 8)\}),(3\mapsto\{(1\mapsto 4),(2\mapsto 3),(3\mapsto 6),(4\mapsto 8),(5\mapsto 9),(6\mapsto 5),(7\mapsto 7),(8\mapsto 1),(9\mapsto 2)\}),(4\mapsto\{(1\mapsto 2),(2\mapsto 4),(3\mapsto 9),(4\mapsto 3),(5\mapsto 7),(6\mapsto 6),(7\mapsto 8),(8\mapsto 5),(9\mapsto 1)\}),(5\mapsto\{(1\mapsto 6),(2\mapsto 7),(3\mapsto 3),(4\mapsto 5),(5\mapsto 8),(6\mapsto 1),(7\mapsto 2),(8\mapsto 9),(9\mapsto 4)\}),(6\mapsto\{(1\mapsto 5),(2\mapsto 1),(3\mapsto 8),(4\mapsto 4),(5\mapsto 2),(6\mapsto 9),(7\mapsto 3),(8\mapsto 6),(9\mapsto 7)\}),(7\mapsto\{(1\mapsto 1),(2\mapsto 9),(3\mapsto 4),(4\mapsto 2),(5\mapsto 6),(6\mapsto 7),(7\mapsto 5),(8\mapsto 8),(9\mapsto 3)\}),(8\mapsto\{(1\mapsto 8),(2\mapsto 6),(3\mapsto 7),(4\mapsto 1),(5\mapsto 5),(6\mapsto 3),(7\mapsto 4),(8\mapsto 2),(9\mapsto 9)\}),(9\mapsto\{(1\mapsto 3),(2\mapsto 2),(3\mapsto 5),(4\mapsto 9),(5\mapsto 4),(6\mapsto 8),(7\mapsto 1),(8\mapsto 7),(9\mapsto 6)\})\}$
* $SUBSQ = \{\{1,2,3\},\{4,5,6\},\{7,8,9\}\}$
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\mapsto 2),(17\mapsto 4),(23\mapsto 0),(24\mapsto 0),(39\mapsto 0),(40\mapsto 0)\}$
* $coins = \{16,17,23,24,39,40\}$
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"\mapsto"Charles"),("butler"\mapsto"Agatha"),("butler"\mapsto"Charles")\}$
* $victim = "Agatha"$
* $killer = "Agatha"$
* $hates = \{("Agatha"\mapsto"Agatha"),("Agatha"\mapsto"Charles"),("Charles"\mapsto"butler"),("butler"\mapsto"Agatha"),("butler"\mapsto"Charles")\}$
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\mapsto 0),(2\mapsto 2),(3\mapsto 6),(4\mapsto 9),(5\mapsto 14),(6\mapsto 24),(7\mapsto 25)\}$
* $len = 25$
* $n = 7$
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\mapsto"c"),(2\mapsto"a"),(3\mapsto"b")\}$
* $n2 = "b"$
* $n3 = "c"$
* $V = \{1,2,3\}$
* $g1 = \{(1\mapsto 2),(1\mapsto 3),(2\mapsto 3)\}$
* $g2 = \{("a"\mapsto"b"),("c"\mapsto"a"),("c"\mapsto"b")\}$
* $v1 = 1$
* $v2 = 2$
* $v3 = 3$
* $N = \{"a","b","c"\}$
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
"abc"
```
%% Output
$"abc"$
"abc"
%% Cell type:code id: tags:
``` prob
```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment