Description

Consider the following game :

There are three players and a deck with 8 cards: 4 aces and 4 eights.
Each agent is dealt two cards and the remaining two cards are left face down. Assuming an ordering for the agents, they take turns trying to determine their own cards by looking at the cards of the others.
When a player is sure about his draw in his turn, he announces it, thus ending the game.

Notation

Cards

At first we need to define all available agents' draws :

1. A_i≔ agent i has a pair of aces
2. E_i≔ agent i has a pair of eights
3. M_i≔ agent i has a mixed draw

Epistemic states

We also need to define the epistemic states aka worlds in the game :

A state is simply the draws for every agent, so it is simply a combination between agents' draws. But we should remember that there are eight cards in total, four for each kind, and that restricts the available choices. After some thought one should end up with the following set of epistemic states :

(A_a,A_b,E_c),(A_a, E_b, A_c), (A_a, E_b, M_c), (A_a, E_b, E_c), (A_a, M_b, E_c),(A_a, M_b, M_c), (E_a,A_b,A_c),(E_a,A_b,E_c), (E_a,A_b,M_c),(E_a,E_b,A_c), (E_a,M_b,A_c),(E_a,M_b,M_c), (M_a,A_b,E_c),(M_a,A_b,M_c), (M_a,E_b,A_c),(M_a,E_b,M_c), (M_a,M_b,A_c),(M_a,M_b,E_c), (M_a,M_b,M_c)

Finally, we may simplify the notation by taking into account the fixed agents' order, so that we call a world XiYjZw as XYZ.

Using Dynamic Epistemic Logic

Visualization as a Kripke structure

We can imagine all XYZ as nodes in an undirected graph. The graph has three types of edges :

• red edges that connect nodes which are the same (knowledge-wise) for agent a i.e. u1∼au2
• green edges that connect nodes which are the same (knowledge-wise) for agent b i.e. u1∼bu2
• blue edges that connect nodes which are the same (knowledge-wise) for agent c i.e. u1∼cu2

For instance, one can easily see above that states AME,AMM are the "same" for agent c since he shall see the same cards from the other two agents regardless of his own draw.

Statements & Announcements

By the usual notation in modal logic, one could express the sentence e.g. "Agent a does not know his draw" as ¬(KaAa∨KaEa∨KaMa)

But what changes such an expression carries?

We could visualize this change by considering its negation i.e. if Agent a could know his draw. If he could tell his draw, then the valid epistemic state could not be confused (by him) with another. Consequently, the equivalence class for ∼_a would contain only one state. So we can safely discard those states, since he cannot really tell his draw (we assume that the agents are not only logical, but always truthful as well).

These changes are, of course, depicted in our graph by removing nodes (and their edges) accordingly. Also, it is important to note that this new information modifies the agents' knowledge universally. For example, in the first round agent b, after hearing that a cannot tell his draw, also knows that a could not have seen two aces or two eights, so he can safely discard states AEE,EAA as well.

Here is the structure after the first agent's announcement that he cannot tell his draw.

Implementation

Main class file

Using Python 3.8 we implemented the above graph approach to the Aces & Eights Puzzle in this file. The whole puzzle is represented by class AcesEightsPuzzle where one can define different agents' names, the draw and whether some output during the game is expected. We are using an undirected graph structure from module NetworkX, its nodes are those described previously and the edges of each agent shall be between nodes that share exactly two individual draws in their respective place (e.g. for red edges we shall have XME⟷YME,XMA⟷YMA etc).

Available functionality includes the removal of nodes for an Agent (after announcing his inability to tell his draw, the simulation of the game for every round until an Agent is sure about his draw and the visualization of the structure in any step of the game (with optional .svg file production) You can run the program by typing in your terminal python aces_eights.py

Unit testing

To test the program's validity we have developed a testing program that enables us to sanity check the methods' correctness. You can find that program here and test your own understanding on the puzzle by considering why each condition is valid. Why is an Agent able to tell (or not) in some state? Why these nodes shall be removed after this Agent announces that he cannot tell?