-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.Puzzles.Birthday
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- This is a formalization of the Cheryl's birthday problem, which went viral in April 2015.
-- (See .)
--
-- Here's the puzzle:
--
-- @
-- Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.
--
-- 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:
--
-- May 15, May 16, May 19
-- June 17, June 18
-- July 14, July 16
-- August 14, August 15, August 17
--
-- “My birthday is one of these,” she said.
--
-- 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.
-- “Can you figure it out now?” she asked Albert.
--
-- Albert: I don’t know when your birthday is, but I know Bernard doesn’t know, either.
-- Bernard: I didn’t know originally, but now I do.
-- Albert: Well, now I know, too!
--
-- When is Cheryl’s birthday?
-- @
--
-- NB. Thanks to Amit Goel for suggesting the formalization strategy used in here.
-----------------------------------------------------------------------------
module Documentation.SBV.Examples.Puzzles.Birthday where
import Data.SBV
-----------------------------------------------------------------------------------------------
-- * Types and values
-----------------------------------------------------------------------------------------------
-- | Represent month by 8-bit words; We can also use an uninterpreted type, but numbers work well here.
type Month = SWord8
-- | Represent day by 8-bit words; Again, an uninterpreted type would work as well.
type Day = SWord8
-- | Months referenced in the problem.
may, june, july, august :: SWord8
[may, june, july, august] = [5, 6, 7, 8]
-----------------------------------------------------------------------------------------------
-- * Helper predicates
-----------------------------------------------------------------------------------------------
-- | Check that a given month/day combo is a possible birth-date.
valid :: Month -> Day -> SBool
valid month day = (month, day) `sElem` candidates
where candidates :: [(Month, Day)]
candidates = [ ( may, 15), ( may, 16), ( may, 19)
, ( june, 17), ( june, 18)
, ( july, 14), ( july, 16)
, (august, 14), (august, 15), (august, 17)
]
-- | Assert that the given function holds for one of the possible days.
existsDay :: (Day -> SBool) -> SBool
existsDay f = sAny (f . literal) [14 .. 19]
-- | Assert that the given function holds for all of the possible days.
forallDay :: (Day -> SBool) -> SBool
forallDay f = sAll (f . literal) [14 .. 19]
-- | Assert that the given function holds for one of the possible months.
existsMonth :: (Month -> SBool) -> SBool
existsMonth f = sAny f [may .. august]
-- | Assert that the given function holds for all of the possible months.
forallMonth :: (Month -> SBool) -> SBool
forallMonth f = sAll f [may .. august]
-----------------------------------------------------------------------------------------------
-- * The puzzle
-----------------------------------------------------------------------------------------------
-- | Encode the conversation as given in the puzzle.
--
-- NB. Lee Pike pointed out that not all the constraints are actually necessary! (Private
-- communication.) The puzzle still has a unique solution if the statements @a1@ and @b1@
-- (i.e., Albert and Bernard saying they themselves do not know the answer) are removed.
-- To experiment you can simply comment out those statements and observe that there still
-- is a unique solution. Thanks to Lee for pointing this out! In fact, it is instructive to
-- assert the conversation line-by-line, and see how the search-space gets reduced in each
-- step.
puzzle :: Predicate
puzzle = do birthDay <- exists "birthDay"
birthMonth <- exists "birthMonth"
-- Albert: I do not know
let a1 m = existsDay $ \d1 -> existsDay $ \d2 ->
d1 ./= d2 .&& valid m d1 .&& valid m d2
-- Albert: I know that Bernard doesn't know
let a2 m = forallDay $ \d -> valid m d .=>
existsMonth (\m1 -> existsMonth $ \m2 ->
m1 ./= m2 .&& valid m1 d .&& valid m2 d)
-- Bernard: I did not know
let b1 d = existsMonth $ \m1 -> existsMonth $ \m2 ->
m1 ./= m2 .&& valid m1 d .&& valid m2 d
-- Bernard: But now I know
let b2p m d = valid m d .&& a1 m .&& a2 m
b2 d = forallMonth $ \m1 -> forallMonth $ \m2 ->
(b2p m1 d .&& b2p m2 d) .=> m1 .== m2
-- Albert: Now I know too
let a3p m d = valid m d .&& a1 m .&& a2 m .&& b1 d .&& b2 d
a3 m = forallDay $ \d1 -> forallDay $ \d2 ->
(a3p m d1 .&& a3p m d2) .=> d1 .== d2
-- Assert all the statements made:
constrain $ a1 birthMonth
constrain $ a2 birthMonth
constrain $ b1 birthDay
constrain $ b2 birthDay
constrain $ a3 birthMonth
-- Find a valid birth-day that satisfies the above constraints:
return $ valid birthMonth birthDay
-- | Find all solutions to the birthday problem. We have:
--
-- >>> cheryl
-- Solution #1:
-- birthDay = 16 :: Word8
-- birthMonth = 7 :: Word8
-- This is the only solution.
cheryl :: IO ()
cheryl = print =<< allSat puzzle