Symbolically finding Cheryl's Birthday with SMCDEL

2019-03-01

This is a follow-up to my previous post Finding Cheryl’s Birthday with DEMO in which I solved the famous puzzle about Cheryl’s Birthday using DEMO, an explicit model checker for Dynamic Epistemic Logic (DEL).

Since this commit the famous puzzle is also one of the examples included in SMCDEL, a symbolic model checker for DEL. Here I will explain the basics usage of SMCDEL and highlight the differences between explicit and symbolic model checking.

Like DEMO, also SMCDEL is meant to be used as a Haskell module. There is also a command-line and a web interface which are easier to use, but as of now they provide less functionality. It would be a hassle to encode Cheryl’s Birthday in the format needed by those interfaces, so here we will use Haskell directly.

We start by importing a Haskell library for lists and two modules from SMCDEL: the language and the symbolic methods for S5. The latter choice makes sense because the puzzle is only about knowledge, not belief.

module SMCDEL.Examples.Cheryl where

import Data.List

import SMCDEL.Language
import SMCDEL.Symbolic.S5

Before doing anything with SMCDEL we define the set of all possibilities, i.e. all birthdays. This is exactly the same as in the DEMO version, but for readability we also introduce a type alias.

type Possibility = (Int, String)

possibilities :: [Possibility]
possibilities =
  [ (15,"May"), (16,"May"), (19,"May")
  , (17,"June"), (18,"June")
  , (14,"July"), (16,"July")
  , (14,"August"), (15,"August"), (17,"August") ]

Recall that DEMO offers many different atomic propositions like P Int, Q Int, R Int and Info a. Especially the Info a propositions are a very convenient and powerful tool. Unfortunately, such nominal propositions are not available in SMCDEL. The language in SMCDEL provides only one set of atomic propositions given by P Int. This restriction is due to the encoding with Binary Decision Diagrams.

Still, also without Info a propositions we can make our life easy: we define abbreviations in Haskell so that we can write formulas more easily. For example, we fix that P 17 means “The day of Cheryl’s birthday is 17.” and that P 8 means “The month of Cheryl’s birthday is August.”

dayIs :: Int -> Prp
dayIs = P

monthIs :: String -> Prp
monthIs "May"    = P 5
monthIs "June"   = P 6
monthIs "July"   = P 7
monthIs "August" = P 8
monthIs _        = undefined

We then combine our atomic propositions to form more complex formulas. For example, the command thisPos (15,"August") will give us the conjunction Conj [PrpF (P 15), PrpF (P 8)] saying that Cheryl’s birthday is the 15th of August. The second formula knWhich i says that agent i knows Cheryl’s birthday. This the same as knowsBday in the DEMO version and also here we define it as a big disjunction. This is not optimal, but given the small model size in this puzzle, it does not hurt.

thisPos :: Possibility -> Form
thisPos (d,m) = Conj $
  (PrpF (dayIs d)   : [ Neg (PrpF $ dayIs d')   | d' <- nub (map fst possibilities) \\ [d] ]) ++
  (PrpF (monthIs m) : [ Neg (PrpF $ monthIs m') | m' <- nub (map snd possibilities) \\ [m] ])

knWhich :: Agent -> Form
knWhich i = Disj [ K i (thisPos pos) | pos <- possibilities ]

Now, instead of an initial Kripke model, for SMCDEL we need a knowledge structure modelling the start of the puzzle. A knowledge structure is the symbolic analogue of a Kripke model. Recall that a Kripke model contains a set of worlds w1, w2, etc. and valuations like p1 : true, p2 : false, etc. for each world. Instead of listing all this information explicitly, a knowledge structure contains a summary of the whole set of worlds.

The main trick of symbolic model checking is to replace the explicit list of worlds with a boolean formula and then say: My worlds are all boolean assignments satisfying this formula.

Well, and there are some more ingredients. First, there are many tricks to find and modify this boolean formula. Second, instead of a formula we only need the boolean function it represents and this can be represented as a Binary Decision Diagram.

A knowledge structure now consists of three parts:

  • a list of propositions called the vocabulary: allprops,
  • the aforementioned boolean formula: statelaw, and
  • for each agent a list which propositions that agent observes: obs.

Let us compare this again to a Kripke model. The vocabulary and state law together replace the set of worlds and the valuation function. The observational variables replace the accessibility relation.

(Maybe you are now wondering whether a knowledge structure is just a different way to write down a Kripke model. The answer is yes. Think of knowledge structures as a data structure to store Kripke models.)

Enough theory, here is the initial knowledge structure for Cheryl’s Birthday puzzle:

start :: KnowStruct
start = KnS allprops statelaw obs where
  allprops = sort $ nub $ map (dayIs . fst) possibilities ++
                          map (monthIs . snd) possibilities
  statelaw = boolBddOf $ Conj
    [ Disj (map thisPos possibilities)
    , Conj [ Neg $ Conj [thisPos p1, thisPos p2]
           | p1 <- possibilities, p2 <- possibilities, p1 /= p2 ] ]
  obs = [ ("Albert" , nub $ map (monthIs . snd) possibilities)
        , ("Bernard", nub $ map (dayIs   . fst) possibilities) ]

It is easy to check that allprobs is the list map P [5,6,7,8,14,15,16,17,18,19]. The formula statelaw essentially says “The birthday must be one of the possibilities, but it cannot be two different ones at the same time.” To encode the knowledge of the agents, we let Albert observe all atomic propositions about the day and Bernard those about the month. An equivalent and sometimes more intuitive way to read observational variables is this: an agent observes a variable iff the agent knows whether that variable is true.

Now we will update the model structure with public announcements, given by the dialogue in the puzzle. The announced formulas are exactly the same as in the DEMO implementation, with small syntax adaptations. Instead of the upd_pa function in DEMO we now use the update function in SMCDEL. In fact, update is polymorphic such that it also accepts action models or transformers, but here it is given a formula and will thus execute a public announcement.

First Albert says: “I don’t know when Cheryl’s birthday is and I know that Bernard does not know.” To model this we update with the following conjunction:

round1 = update start (Conj [ Neg $ knWhich "Albert"
                            , K "Albert" $ Neg (knWhich "Bernard")])

Then Bernard says: “Now I know when Cheryl’s birthday is.”

round2 = update round1 (knWhich "Bernard")

Finally, Albert says: “Now I also know when Cheryl’s birthday is.”

round3 = update round2 (knWhich "Albert")

We can now get the solution by asking for the remaining states:

$ stack ghci src/SMCDEL/Examples/Cheryl.hs
λ> statesOf round3
[[P 7,P 16]]

To get the solution in a more readable form, we can write a little helper function:

cherylsBirthday :: String
cherylsBirthday = m ++ " " ++ show d ++ "th" where
  [(d,m)] = filter
    (\(d',m') -> [monthIs m', dayIs d'] `elem` statesOf round3)
    possibilities

Spoiler alert!

λ> cherylsBirthday
"July 16th"

If you want to learn more about the internals of SMCDEL, please have a look at the source code and documentation or my PhD thesis. The first chapter also describes the basics of Dynamic Epistemic Logic.