Cheryl.hs

------------------------------------------------------------------------------------------
-- A formalization of the Cheryl's birtday problem; using Haskell/SBV
--
-- See: http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
--
-- By Levent Erkok, This file is in the public domain. Use it as you wish!
--
-- NB. Thanks to Amit Goel for suggesting the formalization strategy used in here.
------------------------------------------------------------------------------------------

module Cheryl(main) where

import Data.SBV

-- Represent month and day by 8-bit words; they are small enough to fit.
type Month = SWord8
type Day   = SWord8

-- Months referenced in the problem:
may, june, july, august :: SWord8
[may, june, july, august] = [5, 6, 7, 8]

-- 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 = bAny (f . literal) [14 .. 19]

-- Assert that the given function holds for all of the possible days
forallDay :: (Day -> SBool) -> SBool
forallDay f = bAll (f . literal) [14 .. 19]

-- Assert that the given function holds for one of the possible months
existsMonth :: (Month -> SBool) -> SBool
existsMonth f = bAny f [may .. august]

-- Assert that the given function holds for all of the possible months
forallMonth :: (Month -> SBool) -> SBool
forallMonth f = bAll f [may .. august]

-- Encode the conversation
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 $ valid birthMonth birthDay
            constrain $ a1 birthMonth
            constrain $ a2 birthMonth
            constrain $ b1 birthDay
            constrain $ b2 birthDay
            constrain $ a3 birthMonth

            -- no extra condition to prove
            return true

-- $ ghci Cheryl.hs
-- *Cheryl> main
-- Solution #1:
--   birthDay = 16 :: Word8
--   birthMonth = 7 :: Word8
-- This is the only solution.
main :: IO ()
main = print =<< allSat puzzle