Cheryl's Birthday

This Puzzle is a variation of another Puzzle (Sum and Product) and has been described in a New York Times article.

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. You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our online ProB Logic Calculator.

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 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

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 in 20-30 ms */
  Month = "july";
  Day = 16
END

When loading this B machine in ProB, you will see that there is only a single solution (solving time 20-30 ms) : Month = "july" and Day = 16.

Here is a screenshot of ProB Tcl/Tk after loading the model.

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}

and then 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 also "july" in the ASSERTIONS clause into july. This makes constraint solving via ProB marginally faster.