Skip to content
Snippets Groups Projects
Commit 93c0b96a authored by penguinn's avatar penguinn
Browse files

Add Overview

parent 8c1dd15c
No related branches found
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 10759 additions and 0 deletions
.ipynb_checkpoints/Bridges_Puzzle-checkpoint.ipynb 0 → 100644
+ 603
− 0
View file @ 93c0b96a
%% Cell type:markdown id: tags:
# Bridges Puzzle (Hashiwokakero)
The [Hashiwokakero](https://en.wikipedia.org/wiki/Hashiwokakero) Puzzle is a logical puzzle where one has to build bridges between islands. The puzzle is also known under the name Ai-Ki-Ai. The puzzles can also be [played online](http://www.puzzle-bridges.com).
The requirements for this puzzle are as follows:
* the goal is to build bridges between islands so as to generate a connected graph
* every island has a number on it, indicating exactly how many bridges should be linked with the island
* there is an upper bound (MAXBRIDGES) on the number of bridges that can be built-between two islands
* bridges cannot cross each other
A B model for this puzzle can be found below. The constants and sets of the model are as follows:
* N are the nodes (islands); we have added a constant ignore where one can stipulate which islands should be ignored in this puzzle
* nl (number of links) stipulates for each island how many bridges it should be linked with
* xc, yc are the x- and y-coordinates for every island
A simple puzzle with four islands would be defined as follows, assuming
the basic set N is defined as `N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}`:
~~~~
xc(a)=0 & xc(b)=1 & xc(c)=0 & xc(d) = 1 &
yc(a)=0 & yc(b)=0 & yc(c)=1 & yc(d) = 1 &
nl = {a|->2, b|->2, c|->2, d|->2} &
ignore = {e,f,g,h,i,j,k,l,m,n}
~~~~
Below we will use a more complicated puzzle to illustrate the B model.
The model then contains the following derived constants:
* plx,ply: the possible links between islands on the x- and y-axis respectively
* pl: the possible links both on the x- and y-axis combined
* cs: the conflict set of links which overlap, i.e., one cannot build bridges on both links (a,b) when the pair (a,b) is in cs
* connected: the set of links on which at least one bridge was built
The model also sets up the goal constant `sol` which maps every link in `pl` to a number indicating how many bridges are built on it. The model also stipulates that the graph set up by connected generates a fully connected graph.
If you need help or want to find out more about jupyter notebook functionalities type in `:help` and `:help COMMAND` for an overview of the commands and a more detailed information about the command.
%% Cell type:code id: tags:
``` prob
::load DOT=/usr/bin/dot
MACHINE Bridges
DEFINITIONS
MAXBRIDGES==2;
LINKS == 1..(MAXBRIDGES*4);
COORD == 0..10;
p1 == prj1(nodes,nodes);
p2 == prj2(nodes,nodes);
p1i == prj1(nodes,INTEGER)
SETS
N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}
CONSTANTS nodes, ignore, nl, xc,yc, plx,ply,pl, cs, sol, connected
PROPERTIES
nodes = N \ ignore &
// target number of links per node:
nl : nodes --> LINKS & /* number of links */
// coordinates of nodes
xc: nodes --> COORD & yc: nodes --> COORD &
// possible links:
pl : nodes <-> nodes &
plx : nodes <-> nodes &
ply : nodes <-> nodes &
plx = {n1,n2 | xc(n1)=xc(n2) & n1 /= n2 & yc(n2)>yc(n1) &
!n3.(xc(n3)=xc(n1) => yc(n3) /: yc(n1)+1..yc(n2)-1) } &
ply = {n1,n2 | yc(n1)=yc(n2) & n1 /= n2 & xc(n2)>xc(n1) &
!n3.(yc(n3)=yc(n1) => xc(n3) /: xc(n1)+1..xc(n2)-1)} &
pl = plx \/ ply &
// compute conflict set (assumes xc,yc coordinates ordered in plx,ply)
cs = {pl1,pl2 | pl1:plx & pl2:ply &
xc(p1(pl1)): xc(p1(pl2))+1..xc(p2(pl2))-1 &
yc(p1(pl2)): yc(p1(pl1))+1..yc(p2(pl1))-1} &
sol : pl --> 0..MAXBRIDGES &
!nn.(nn:nodes => SIGMA(l).(l:pl &
(p1(l)=nn or p2(l)=nn)|sol(l))=nl(nn)) &
!(pl1,pl2).( (pl1,pl2):cs => sol(pl1)=0 or sol(pl2)=0) & // no conflicts
// check graph connected
connected = {pl|sol(pl)>0} &
closure1(connected \/ connected~)[{a}] = {nn|nn:nodes & nl(nn)>0} &
// encoding of puzzle
// A puzzle from bridges.png
xc(a)=1 & yc(a)=1 & nl(a)=4 &
xc(b)=1 & yc(b)=4 & nl(b)=6 &
xc(c)=1 & yc(c)=6 & nl(c)=3 &
xc(d)=2 & yc(d)=2 & nl(d)=1 &
xc(e)=2 & yc(e)=5 & nl(e)=2 &
xc(f)=3 & yc(f)=2 & nl(f)=4 &
xc(g)=3 & yc(g)=4 & nl(g)=6 &
xc(h)=3 & yc(h)=5 & nl(h)=4 &
xc(i)=4 & yc(i)=3 & nl(i)=3 &
xc(j)=4 & yc(j)=6 & nl(j)=3 &
xc(k)=5 & yc(k)=2 & nl(k)=1 &
xc(l)=6 & yc(l)=1 & nl(l)=4 &
xc(m)=6 & yc(m)=3 & nl(m)=5 &
xc(n)=6 & yc(n)=5 & nl(n)=2 &
ignore = {}
END
```
%% Output
Loaded machine: Bridges
%% 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:
After setting the constants and initialising the machine with the above commands, one can see that the solution for this puzzle, which is saved in `sol`, is the following:
(Simply type in `sol` to get the value for it.)
%% Cell type:code id: tags:
``` prob
sol
```
%% Output
$\{(\mathit{a}\mapsto \mathit{b}\mapsto 2),(\mathit{a}\mapsto \mathit{l}\mapsto 2),(\mathit{b}\mapsto \mathit{c}\mapsto 2),(\mathit{b}\mapsto \mathit{g}\mapsto 2),(\mathit{c}\mapsto \mathit{j}\mapsto 1),(\mathit{d}\mapsto \mathit{e}\mapsto 0),(\mathit{d}\mapsto \mathit{f}\mapsto 1),(\mathit{e}\mapsto \mathit{h}\mapsto 2),(\mathit{f}\mapsto \mathit{g}\mapsto 2),(\mathit{f}\mapsto \mathit{k}\mapsto 1),(\mathit{g}\mapsto \mathit{h}\mapsto 2),(\mathit{h}\mapsto \mathit{n}\mapsto 0),(\mathit{i}\mapsto \mathit{j}\mapsto 2),(\mathit{i}\mapsto \mathit{m}\mapsto 1),(\mathit{l}\mapsto \mathit{m}\mapsto 2),(\mathit{m}\mapsto \mathit{n}\mapsto 2)\}$
{(a↦b↦2),(a↦l↦2),(b↦c↦2),(b↦g↦2),(c↦j↦1),(d↦e↦0),(d↦f↦1),(e↦h↦2),(f↦g↦2),(f↦k↦1),(g↦h↦2),(h↦n↦0),(i↦j↦2),(i↦m↦1),(l↦m↦2),(m↦n↦2)}
%% Cell type:markdown id: tags:
## Adding Graphical Visualisation
To show the solution graphically, we can add the following to the
`DEFINITIONS` clause in the model:
~~~~
CUSTOM_GRAPH_NODES == {n,w,w2|(n|->w):nl & w=w2}; // %n1.(n1:nodes|nl(n1));
CUSTOM_GRAPH_EDGES == {n1,w,n2|n1:nl & n2:nl & (p1i(n1),p1i(n2),w):sol}
~~~~
%% Cell type:code id: tags:
``` prob
::load DOT=/usr/bin/dot
MACHINE Bridges
DEFINITIONS
MAXBRIDGES==2;
LINKS == 1..(MAXBRIDGES*4);
COORD == 0..10;
p1 == prj1(nodes,nodes);
p2 == prj2(nodes,nodes);
p1i == prj1(nodes,INTEGER);
CUSTOM_GRAPH_NODES == {n,w,w2|(n|->w):nl & w=w2}; // %n1.(n1:nodes|nl(n1));
CUSTOM_GRAPH_EDGES == {n1,w,n2|n1:nl & n2:nl & (p1i(n1),p1i(n2),w):sol}
SETS
N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}
CONSTANTS nodes, ignore, nl, xc,yc, plx,ply,pl, cs, sol, connected
PROPERTIES
nodes = N \ ignore &
// target number of links per node:
nl : nodes --> LINKS & /* number of links */
// coordinates of nodes
xc: nodes --> COORD & yc: nodes --> COORD &
// possible links:
pl : nodes <-> nodes &
plx : nodes <-> nodes &
ply : nodes <-> nodes &
plx = {n1,n2 | xc(n1)=xc(n2) & n1 /= n2 & yc(n2)>yc(n1) &
!n3.(xc(n3)=xc(n1) => yc(n3) /: yc(n1)+1..yc(n2)-1) } &
ply = {n1,n2 | yc(n1)=yc(n2) & n1 /= n2 & xc(n2)>xc(n1) &
!n3.(yc(n3)=yc(n1) => xc(n3) /: xc(n1)+1..xc(n2)-1)} &
pl = plx \/ ply &
// compute conflict set (assumes xc,yc coordinates ordered in plx,ply)
cs = {pl1,pl2 | pl1:plx & pl2:ply &
xc(p1(pl1)): xc(p1(pl2))+1..xc(p2(pl2))-1 &
yc(p1(pl2)): yc(p1(pl1))+1..yc(p2(pl1))-1} &
sol : pl --> 0..MAXBRIDGES &
!nn.(nn:nodes => SIGMA(l).(l:pl &
(p1(l)=nn or p2(l)=nn)|sol(l))=nl(nn)) &
!(pl1,pl2).( (pl1,pl2):cs => sol(pl1)=0 or sol(pl2)=0) & // no conflicts
// check graph connected
connected = {pl|sol(pl)>0} &
closure1(connected \/ connected~)[{a}] = {nn|nn:nodes & nl(nn)>0} &
// encoding of puzzle
// A puzzle from bridges.png
xc(a)=1 & yc(a)=1 & nl(a)=4 &
xc(b)=1 & yc(b)=4 & nl(b)=6 &
xc(c)=1 & yc(c)=6 & nl(c)=3 &
xc(d)=2 & yc(d)=2 & nl(d)=1 &
xc(e)=2 & yc(e)=5 & nl(e)=2 &
xc(f)=3 & yc(f)=2 & nl(f)=4 &
xc(g)=3 & yc(g)=4 & nl(g)=6 &
xc(h)=3 & yc(h)=5 & nl(h)=4 &
xc(i)=4 & yc(i)=3 & nl(i)=3 &
xc(j)=4 & yc(j)=6 & nl(j)=3 &
xc(k)=5 & yc(k)=2 & nl(k)=1 &
xc(l)=6 & yc(l)=1 & nl(l)=4 &
xc(m)=6 & yc(m)=3 & nl(m)=5 &
xc(n)=6 & yc(n)=5 & nl(n)=2 &
ignore = {}
END
```
%% Output
Loaded machine: Bridges
%% 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:
One can then initialise the model, as above and the execute the command `:dot custom_graph`. This leads to the following picture:
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:code id: tags:
``` prob
```
.ipynb_checkpoints/Cheryls_Birthday-checkpoint.ipynb 0 → 100644
+ 404
− 0
View file @ 93c0b96a
%% Cell type:markdown id: tags:
# Cheryl's Birthday
This Puzzle is a variation of another Puzzle (Sum and Product) and has
been described
in a New York Times article(http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html).
Here is a first solution in B, where the text of the puzzle has been
integrated as comments. There are almost certainly more elegant
encodings of the problem in B.
In case you are new to B, you probably need to know the following
operators to understand the specification below (we als have a
<<summary-of-b-syntax,summary page about the B syntax>>):
* `x : S` specifies that x is an element of S
* `dom(r)` is the domain of a function or relation r
* `r~` is the inverse of a function or relation r
* `r[S]` is the relational image of a relation r for a set of domain values S
* `card(S)` is the cardinality of a set S
* `a|->b` represents the pair (a,b); note that a relation and function in B is a set of pairs.
* `!x.(P => Q)` denotes universal quantification over variable x
In case you are new to using the jupyter notebook, simply type in `:help` to get an overview over the full range of options you have with the ProB core.
%% Cell type:code id: tags:
``` prob
::load
MACHINE CherylsBirthday
/* A simplified version of the SumProduct Puzzle taken from
http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
*/
DEFINITIONS
DontKnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) > 1;
KnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) = 1
CONSTANTS Month, Day, PD, PD2
PROPERTIES
/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/
Month:STRING & Day:1..31 &
/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */
PD = {("aug"|->14),("aug"|->15),("aug"|->17),
("july"|->14),("july"|->16),("june"|->17),("june"|->18),
("may"|->15),("may"|->16),("may"|->19)}
&
/*
Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday.
To Bernard, she whispered the day, and only the day.
*/
Month : dom(PD) &
Day : ran(PD) &
Month|->Day : PD &
/* Albert: I don’t know when your birthday is, */
card(PD[{Month}]) > 1 &
/* but I know Bernard doesn’t know, either. */
!x.(x:PD[{Month}] => DontKnowFromDay(PD,x) ) &
/* Bernard: I didn’t know originally, */
DontKnowFromDay(PD,Day) &
/* but now I do. */
PD2 = {m,d| (m|->d):PD & !x.(x:PD[{m}] => DontKnowFromDay(PD,x) ) } &
KnowFromDay(PD2,Day) &
/* Albert: Well, now I know, too! */
card({d|Month|->d : PD2 & KnowFromDay(PD2,d)})=1
ASSERTIONS /* single solution found by ProB */
Month = "july";
Day = 16
END
```
%% Output
Loaded machine: CherylsBirthday
%% Cell type:markdown id: tags:
After loading this B machine, you will see that there is only a single solution (solving time 20-30 ms) : `Month = "july"` and `Day = 16`.
With jupyter notebook, you have to type in `:constants` to set up the models constants.
After doing that, you can use `:init` to initialise your machine.
%% 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:
You can check for the solution simply by typing in `Month` and `Day`. You will see, there is only one solution for this problem.
%% Cell type:code id: tags:
``` prob
Month
```
%% Output
$\text{"july"}$
"july"
%% Cell type:code id: tags:
``` prob
Day
```
%% Output
$16$
16
%% Cell type:markdown id: tags:
## Using an enumerated set
It is possible to use an enumerated set for the Months. One simply has to add:
~~~~
SETS MONTHS = {may, june, july, aug, sep}
~~~~
change the definition of the possible dates:
~~~~
PD = {(aug|->14), (aug|->15), (aug|->17),
(july|->14),(july|->16),(june|->17),
(june|->18),
(may|->15),(may|->16),(may|->19)}
~~~~
and change the type of Month to `MONTHS`. This possible solution makes the constraint solving via ProB marginally faster.
%% Cell type:code id: tags:
``` prob
::load
MACHINE CherylsBirthday
/* A simplified version of the SumProduct Puzzle taken from
http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
*/
DEFINITIONS
DontKnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) > 1;
KnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) = 1
SETS
MONTHS = {may, june, july, aug, sep}
CONSTANTS Month, Day, PD, PD2
PROPERTIES
/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/
Month:MONTHS & Day:1..31 &
/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */
PD = {(aug|->14), (aug|->15), (aug|->17),
(july|->14),(july|->16),(june|->17),
(june|->18),
(may|->15),(may|->16),(may|->19)}
&
/*
Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday.
To Bernard, she whispered the day, and only the day.
*/
Month : dom(PD) &
Day : ran(PD) &
Month|->Day : PD &
/* Albert: I don’t know when your birthday is, */
card(PD[{Month}]) > 1 &
/* but I know Bernard doesn’t know, either. */
!x.(x:PD[{Month}] => DontKnowFromDay(PD,x) ) &
/* Bernard: I didn’t know originally, */
DontKnowFromDay(PD,Day) &
/* but now I do. */
PD2 = {m,d| (m|->d):PD & !x.(x:PD[{m}] => DontKnowFromDay(PD,x) ) } &
KnowFromDay(PD2,Day) &
/* Albert: Well, now I know, too! */
card({d|Month|->d : PD2 & KnowFromDay(PD2,d)})=1
ASSERTIONS /* single solution found by ProB */
Month = july;
Day = 16
END
```
%% Output
Loaded machine: CherylsBirthday
%% 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:
One will get one possible solution with this code as well. By typing in `Month` and `Day` again, it is possible to check this.
%% Cell type:code id: tags:
``` prob
Month
```
%% Output
$\mathit{july}$
july
%% Cell type:code id: tags:
``` prob
Day
```
%% Output
$16$
16
%% Cell type:code id: tags:
``` prob
```
.ipynb_checkpoints/N_Queens-checkpoint.ipynb 0 → 100644
+ 1893
− 0
View file @ 93c0b96a
This diff is collapsed.
.ipynb_checkpoints/ProB_Jupyter_Notebook_Overview-checkpoint.ipynb 0 → 100644
+ 2475
− 0
View file @ 93c0b96a
This diff is collapsed.
Bridges_Puzzle.ipynb 0 → 100644
+ 612
− 0
View file @ 93c0b96a
This diff is collapsed.
Cheryls_Birthday.ipynb 0 → 100644
+ 404
− 0
View file @ 93c0b96a
%% Cell type:markdown id: tags:
# Cheryl's Birthday
This Puzzle is a variation of another Puzzle (Sum and Product) and has
been described
in a New York Times article(http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html).
Here is a first solution in B, where the text of the puzzle has been
integrated as comments. There are almost certainly more elegant
encodings of the problem in B.
In case you are new to B, you probably need to know the following
operators to understand the specification below (we als have a
<<summary-of-b-syntax,summary page about the B syntax>>):
* `x : S` specifies that x is an element of S
* `dom(r)` is the domain of a function or relation r
* `r~` is the inverse of a function or relation r
* `r[S]` is the relational image of a relation r for a set of domain values S
* `card(S)` is the cardinality of a set S
* `a|->b` represents the pair (a,b); note that a relation and function in B is a set of pairs.
* `!x.(P => Q)` denotes universal quantification over variable x
In case you are new to using the jupyter notebook, simply type in `:help` to get an overview over the full range of options you have with the ProB core.
%% Cell type:code id: tags:
``` prob
::load
MACHINE CherylsBirthday
/* A simplified version of the SumProduct Puzzle taken from
http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
*/
DEFINITIONS
DontKnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) > 1;
KnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) = 1
CONSTANTS Month, Day, PD, PD2
PROPERTIES
/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/
Month:STRING & Day:1..31 &
/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */
PD = {("aug"|->14),("aug"|->15),("aug"|->17),
("july"|->14),("july"|->16),("june"|->17),("june"|->18),
("may"|->15),("may"|->16),("may"|->19)}
&
/*
Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday.
To Bernard, she whispered the day, and only the day.
*/
Month : dom(PD) &
Day : ran(PD) &
Month|->Day : PD &
/* Albert: I don’t know when your birthday is, */
card(PD[{Month}]) > 1 &
/* but I know Bernard doesn’t know, either. */
!x.(x:PD[{Month}] => DontKnowFromDay(PD,x) ) &
/* Bernard: I didn’t know originally, */
DontKnowFromDay(PD,Day) &
/* but now I do. */
PD2 = {m,d| (m|->d):PD & !x.(x:PD[{m}] => DontKnowFromDay(PD,x) ) } &
KnowFromDay(PD2,Day) &
/* Albert: Well, now I know, too! */
card({d|Month|->d : PD2 & KnowFromDay(PD2,d)})=1
ASSERTIONS /* single solution found by ProB */
Month = "july";
Day = 16
END
```
%% Output
Loaded machine: CherylsBirthday
%% Cell type:markdown id: tags:
After loading this B machine, you will see that there is only a single solution (solving time 20-30 ms) : `Month = "july"` and `Day = 16`.
With jupyter notebook, you have to type in `:constants` to set up the models constants.
After doing that, you can use `:init` to initialise your machine.
%% 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:
You can check for the solution simply by typing in `Month` and `Day`. You will see, there is only one solution for this problem.
%% Cell type:code id: tags:
``` prob
Month
```
%% Output
$\text{"july"}$
"july"
%% Cell type:code id: tags:
``` prob
Day
```
%% Output
$16$
16
%% Cell type:markdown id: tags:
## Using an enumerated set
It is possible to use an enumerated set for the Months. One simply has to add:
~~~~
SETS MONTHS = {may, june, july, aug, sep}
~~~~
change the definition of the possible dates:
~~~~
PD = {(aug|->14), (aug|->15), (aug|->17),
(july|->14),(july|->16),(june|->17),
(june|->18),
(may|->15),(may|->16),(may|->19)}
~~~~
and change the type of Month to `MONTHS`. This possible solution makes the constraint solving via ProB marginally faster.
%% Cell type:code id: tags:
``` prob
::load
MACHINE CherylsBirthday
/* A simplified version of the SumProduct Puzzle taken from
http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
*/
DEFINITIONS
DontKnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) > 1;
KnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) = 1
SETS
MONTHS = {may, june, july, aug, sep}
CONSTANTS Month, Day, PD, PD2
PROPERTIES
/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/
Month:MONTHS & Day:1..31 &
/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */
PD = {(aug|->14), (aug|->15), (aug|->17),
(july|->14),(july|->16),(june|->17),
(june|->18),
(may|->15),(may|->16),(may|->19)}
&
/*
Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday.
To Bernard, she whispered the day, and only the day.
*/
Month : dom(PD) &
Day : ran(PD) &
Month|->Day : PD &
/* Albert: I don’t know when your birthday is, */
card(PD[{Month}]) > 1 &
/* but I know Bernard doesn’t know, either. */
!x.(x:PD[{Month}] => DontKnowFromDay(PD,x) ) &
/* Bernard: I didn’t know originally, */
DontKnowFromDay(PD,Day) &
/* but now I do. */
PD2 = {m,d| (m|->d):PD & !x.(x:PD[{m}] => DontKnowFromDay(PD,x) ) } &
KnowFromDay(PD2,Day) &
/* Albert: Well, now I know, too! */
card({d|Month|->d : PD2 & KnowFromDay(PD2,d)})=1
ASSERTIONS /* single solution found by ProB */
Month = july;
Day = 16
END
```
%% Output
Loaded machine: CherylsBirthday
%% 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:
One will get one possible solution with this code as well. By typing in `Month` and `Day` again, it is possible to check this.
%% Cell type:code id: tags:
``` prob
Month
```
%% Output
$\mathit{july}$
july
%% Cell type:code id: tags:
``` prob
Day
```
%% Output
$16$
16
%% Cell type:code id: tags:
``` prob
```
N_Queens.ipynb 0 → 100644
+ 1893
− 0
View file @ 93c0b96a
This diff is collapsed.
ProB_Jupyter_Notebook_Overview.ipynb 0 → 100644
+ 2475
− 0
View file @ 93c0b96a
This diff is collapsed.
images/B_CallButtonDown_Off.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButtonDown_Off.gif

762 B

images/B_CallButtonDown_On.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButtonDown_On.gif

759 B

images/B_CallButtonOff.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButtonOff.gif

235 B

images/B_CallButtonOn.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButtonOn.gif

293 B

images/B_CallButtonUp_Off.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButtonUp_Off.gif

769 B

images/B_CallButtonUp_On.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButtonUp_On.gif

767 B

images/B_CallButton_DownArrow_On.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButton_DownArrow_On.gif

2.57 KiB

images/B_CallButton_UpArrow_On.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButton_UpArrow_On.gif

2.58 KiB

images/B_CallButton_UpDownArrows_Off.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_CallButton_UpDownArrows_Off.gif

1.56 KiB

images/B_DownButton_On.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_DownButton_On.gif

1.32 KiB

images/B_LiftClosed.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_LiftClosed.gif

3.74 KiB

images/B_LiftOpen.gif 0 → 100644
+ 0
− 0
View file @ 93c0b96a
images/B_LiftOpen.gif

3.32 KiB

0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment