sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Puzzles.Birthday

Contents

- Types and values
- Helper predicates
- The puzzle

Description

This is a formalization of the Cheryl's birthday problem, which went viral in April 2015. (See http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html.)

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.

Synopsis

- type Month = SWord8
- type Day = SWord8
- may :: SWord8
- june :: SWord8
- july :: SWord8
- august :: SWord8
- valid :: Month -> Day -> SBool
- existsDay :: (Day -> SBool) -> SBool
- forallDay :: (Day -> SBool) -> SBool
- existsMonth :: (Month -> SBool) -> SBool
- forallMonth :: (Month -> SBool) -> SBool
- puzzle :: Predicate
- cheryl :: IO ()

# Types and values

type Month = SWord8 Source #

Represent month by 8-bit words; We can also use an uninterpreted type, but numbers work well here.

type Day = SWord8 Source #

Represent day by 8-bit words; Again, an uninterpreted type would work as well.

may :: SWord8 Source #

Months referenced in the problem.

june :: SWord8 Source #

Months referenced in the problem.

july :: SWord8 Source #

Months referenced in the problem.

august :: SWord8 Source #

Months referenced in the problem.

# Helper predicates

valid :: Month -> Day -> SBool Source #

Check that a given month/day combo is a possible birth-date.

existsDay :: (Day -> SBool) -> SBool Source #

Assert that the given function holds for one of the possible days.

forallDay :: (Day -> SBool) -> SBool Source #

Assert that the given function holds for all of the possible days.

existsMonth :: (Month -> SBool) -> SBool Source #

Assert that the given function holds for one of the possible months.

forallMonth :: (Month -> SBool) -> SBool Source #

Assert that the given function holds for all of the possible months.

# The puzzle

puzzle :: Predicate Source #

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.

cheryl :: IO () Source #

Find all solutions to the birthday problem. We have:

    >>> cheryl
    Solution #1:
      birthDay   = 16 :: Word8
      birthMonth =  7 :: Word8
    This is the only solution.