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

add short explanation

parent a9d035d4
Branches
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
# SEND-MORE-MONEY
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
In this jupyter notebook, we will take a look on how to solve the famous [verbal arithmetic SEND-MORE-MONEY](https://en.wikipedia.org/wiki/Verbal_arithmetic) puzzle. The task is to find the digits S,E,N,D,M,O,R,Y such that the addition of SEND to MORE leads the decimal number MONEY.
The quickest way is to use the ProB Logic Calculator, which is implemented in Jupyter notebook. To solve the puzzle, simply type in:
`{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` and press enter:
%% 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
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 8$
* $\mathit{S} = 9$
* $\mathit{D} = 7$
* $\mathit{E} = 5$
* $\mathit{Y} = 2$
* $\mathit{M} = 1$
* $\mathit{N} = 6$
* $\mathit{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:
## Explanation
Now let us review the individual conjuncts of the B encoding of the puzzle: The following specifies that S,E,N,D,M,O,R,Y are all digits.
Note that `<:` is the subset operator in B:
`{S,E,N,D, M,O,R, Y} <: 0..9`
An alternative, slightly longer, encoding would have been to write:
`S:0..9 & E:0..9 & N:0..9 & D:0..9 & M:0..9 & O:0..9 & R:0..9 & Y:0..9`
The following conjunct specifies that the S and M cannot be 0:
`S>0 & M>0`
The next conjunct specifies that all digits are distinct:
`card({S,E,N,D, M,O,R, Y})=8`
Note that an alternative, but much longer encoding would have been to specify inequalities:
`S /= E & S /= N & S /= D & … & R/=Y`
Finally, the last conjunct expresses the sum constraint:
`S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y`
%% Cell type:markdown id: tags:
## Alternative Solutions
We are still not sure if this is the only solution. One way to ensure this is to compute a set comprehension with all solutions:
`{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}`
%% 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:
## Wrapping predicate into B machine
Another alternative is to wrap the predicate into a full B machine with the following content:
%% Cell type:code id: tags:
``` prob
::load
MACHINE SendMoreMoney
CONSTANTS S,E,N,D, M,O,R, Y
PROPERTIES
{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
END
```
%% Output
Loaded machine: SendMoreMoney
%% Cell type:markdown id: tags:
To run this example, you will need to setup the constants and initialise the machine with the following commands:
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:markdown id: tags:
To see the result, we will create the following table:
%% Cell type:code id: tags:
``` prob
:table (S,E,N,D, M,O,R, Y)
```
%% Output
|S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---|
|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|
S E N D M O R Y
9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags:
## KISS * KISS = PASSION
A similar puzzle, this times involving multiplication is the KISS * KISS = PASSION puzzle.
Here we again have distinct digits K, I, S, P, A, O, N such that the square of KISS equals the decimal number passion.
The puzzle can be described and solved in a fashion very similar to the problem above:
`{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`
%% Cell type:markdown id: tags:
To make sure, that we don't use the variables from our machine loaded above, we reset our machine to be empty:
%% Cell type:code id: tags:
``` prob
::load
MACHINE empty
END
```
%% Output
Loaded machine: empty
%% 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
$\mathit{TRUE}$
**Solution:**
* $\mathit{P} = 4$
* $\mathit{A} = 1$
* $\mathit{S} = 3$
* $\mathit{I} = 0$
* $\mathit{K} = 2$
* $\mathit{N} = 9$
* $\mathit{O} = 8$
TRUE
Solution:
P = 4
A = 1
S = 3
I = 0
K = 2
N = 9
O = 8
%% Cell type:markdown id: tags:
## Another Puzzle
```
ABC
DEF
+ GHI
-----
123J
```
Each letter is a distinct digit 0-9. What is J?
[A solution is available here.](https://twitter.com/joe_antognini/status/1436044846028902408)
%% Cell type:code id: tags:
``` prob
{A,B,C,D,E,F,G,H,I,J} <: 0..9 &
card({A,B,C,D,E,F,G,H,I,J}) = 10 &
A*100 + B*10 + C +
D*100 + E*10 + F +
G*100 + H*10 + I =
1230 + J
& A>D & D>G & B>E & E>H & C>F & F>I // symmetry breaking
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{A} = 8$
* $\mathit{B} = 7$
* $\mathit{C} = 9$
* $\mathit{D} = 2$
* $\mathit{E} = 5$
* $\mathit{F} = 4$
* $\mathit{G} = 1$
* $\mathit{H} = 0$
* $\mathit{I} = 3$
* $\mathit{J} = 6$
TRUE
Solution:
A = 8
B = 7
C = 9
D = 2
E = 5
F = 4
G = 1
H = 0
I = 3
J = 6
%% Cell type:markdown id: tags:
We can compute all solutions using a set comprehension:
%% Cell type:code id: tags:
``` prob
{A,B,C,D,E,F,G,H,I,J |
:table {A,B,C,D,E,F,G,H,I,J |
{A,B,C,D,E,F,G,H,I,J} <: 0..9 &
card({A,B,C,D,E,F,G,H,I,J}) = 10 &
A*100 + B*10 + C +
D*100 + E*10 + F +
G*100 + H*10 + I =
1230 + J
& A>D & D>G & B>E & E>H & C>F & F>I
}
```
%% Output
$\{(5\mapsto 8\mapsto 9\mapsto 4\mapsto 3\mapsto 7\mapsto 2\mapsto 1\mapsto 0\mapsto 6),(5\mapsto 9\mapsto 8\mapsto 4\mapsto 3\mapsto 7\mapsto 2\mapsto 0\mapsto 1\mapsto 6),(7\mapsto 8\mapsto 9\mapsto 3\mapsto 4\mapsto 5\mapsto 1\mapsto 0\mapsto 2\mapsto 6),(7\mapsto 8\mapsto 9\mapsto 4\mapsto 3\mapsto 5\mapsto 0\mapsto 1\mapsto 2\mapsto 6),(7\mapsto 9\mapsto 8\mapsto 4\mapsto 2\mapsto 5\mapsto 0\mapsto 1\mapsto 3\mapsto 6),(8\mapsto 5\mapsto 9\mapsto 2\mapsto 4\mapsto 7\mapsto 1\mapsto 3\mapsto 0\mapsto 6),(8\mapsto 7\mapsto 9\mapsto 2\mapsto 5\mapsto 4\mapsto 1\mapsto 0\mapsto 3\mapsto 6),(8\mapsto 7\mapsto 9\mapsto 3\mapsto 4\mapsto 5\mapsto 0\mapsto 1\mapsto 2\mapsto 6),(8\mapsto 9\mapsto 7\mapsto 2\mapsto 3\mapsto 5\mapsto 1\mapsto 0\mapsto 4\mapsto 6),(8\mapsto 9\mapsto 7\mapsto 3\mapsto 2\mapsto 5\mapsto 0\mapsto 1\mapsto 4\mapsto 6),(9\mapsto 5\mapsto 8\mapsto 2\mapsto 4\mapsto 7\mapsto 0\mapsto 3\mapsto 1\mapsto 6),(9\mapsto 7\mapsto 8\mapsto 2\mapsto 4\mapsto 5\mapsto 0\mapsto 1\mapsto 3\mapsto 6),(9\mapsto 8\mapsto 7\mapsto 2\mapsto 3\mapsto 5\mapsto 0\mapsto 1\mapsto 4\mapsto 6)\}$
{(5↦8↦9↦4↦3↦7↦2↦1↦0↦6),(5↦9↦8↦4↦3↦7↦2↦0↦1↦6),(7↦8↦9↦3↦4↦5↦1↦0↦2↦6),(7↦8↦9↦4↦3↦5↦0↦1↦2↦6),(7↦9↦8↦4↦2↦5↦0↦1↦3↦6),(8↦5↦9↦2↦4↦7↦1↦3↦0↦6),(8↦7↦9↦2↦5↦4↦1↦0↦3↦6),(8↦7↦9↦3↦4↦5↦0↦1↦2↦6),(8↦9↦7↦2↦3↦5↦1↦0↦4↦6),(8↦9↦7↦3↦2↦5↦0↦1↦4↦6),(9↦5↦8↦2↦4↦7↦0↦3↦1↦6),(9↦7↦8↦2↦4↦5↦0↦1↦3↦6),(9↦8↦7↦2↦3↦5↦0↦1↦4↦6)}
|A|B|C|D|E|F|G|H|I|J|
|---|---|---|---|---|---|---|---|---|---|
|$5$|$8$|$9$|$4$|$3$|$7$|$2$|$1$|$0$|$6$|
|$5$|$9$|$8$|$4$|$3$|$7$|$2$|$0$|$1$|$6$|
|$7$|$8$|$9$|$3$|$4$|$5$|$1$|$0$|$2$|$6$|
|$7$|$8$|$9$|$4$|$3$|$5$|$0$|$1$|$2$|$6$|
|$7$|$9$|$8$|$4$|$2$|$5$|$0$|$1$|$3$|$6$|
|$8$|$5$|$9$|$2$|$4$|$7$|$1$|$3$|$0$|$6$|
|$8$|$7$|$9$|$2$|$5$|$4$|$1$|$0$|$3$|$6$|
|$8$|$7$|$9$|$3$|$4$|$5$|$0$|$1$|$2$|$6$|
|$8$|$9$|$7$|$2$|$3$|$5$|$1$|$0$|$4$|$6$|
|$8$|$9$|$7$|$3$|$2$|$5$|$0$|$1$|$4$|$6$|
|$9$|$5$|$8$|$2$|$4$|$7$|$0$|$3$|$1$|$6$|
|$9$|$7$|$8$|$2$|$4$|$5$|$0$|$1$|$3$|$6$|
|$9$|$8$|$7$|$2$|$3$|$5$|$0$|$1$|$4$|$6$|
A B C D E F G H I J
5 8 9 4 3 7 2 1 0 6
5 9 8 4 3 7 2 0 1 6
7 8 9 3 4 5 1 0 2 6
7 8 9 4 3 5 0 1 2 6
7 9 8 4 2 5 0 1 3 6
8 5 9 2 4 7 1 3 0 6
8 7 9 2 5 4 1 0 3 6
8 7 9 3 4 5 0 1 2 6
8 9 7 2 3 5 1 0 4 6
8 9 7 3 2 5 0 1 4 6
9 5 8 2 4 7 0 3 1 6
9 7 8 2 4 5 0 1 3 6
9 8 7 2 3 5 0 1 4 6
%% Cell type:markdown id: tags:
By using the range operator we can find all possible values for J:
%% Cell type:code id: tags:
``` prob
ran({A,B,C,D,E,F,G,H,I,J |
{A,B,C,D,E,F,G,H,I,J} <: 0..9 &
card({A,B,C,D,E,F,G,H,I,J}) = 10 &
A*100 + B*10 + C +
D*100 + E*10 + F +
G*100 + H*10 + I =
1230 + J
& A>D & D>G & B>E & E>H & C>F & F>I
})
```
%% Output
$\{6\}$
{6}
%% Cell type:code id: tags:
``` prob
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment