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