EpiPEn

Epistemic Programming Environment

by Josh Horowitz and Jack Zhang

Cheryl’s Birthday

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.

Cheryl’s Birthday

May 15, May 16, May 19, June 17, June 18, July 14, July 16, August 14, August 15, August 17.

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!

Cheryl’s Birthday

Albert (knowing the month): I don’t know when your birthday is...

Birthdays, grouped:

​

Can’t eliminate anything

Cheryl’s Birthday

Albert (knowing the month): ...but I know Bernard doesn’t know either.

Birthdays, grouped:

​

Can eliminate two days

Cheryl’s Birthday

Albert (knowing the month): ...but I know Bernard doesn’t know either.

Birthdays, grouped:

​

Can eliminate first two rows

Cheryl’s Birthday

Bernard (knowing the day): I didn't know originally, but now I do.

Birthdays, grouped:

​

Can eliminate two days

Cheryl’s Birthday

Albert (knowing the month): Well, now I know too!

Birthdays, grouped:

​

Can eliminate two days

Cheryl’s Birthday

Albert (knowing the month): Well, now I know too!

Birthdays, grouped:

​

July 16 is the answer

Epistemic Puzzles

• Puzzles that involves knowledge and ignorance
• Solving requires analyzing how the world/common knowledge changes with each announcement
• Solving by hand is error-prone and time-consuming
• We developed a DSL that helps with solving these puzzles

Demo

Logical encoding: stories & knowledge states

A “story” starts with a set { A_i } of “characters” and a set { x_i } of unknown constants.

e.g., { A_i } = { Albert, Bernard }, { x_i } = { bday month, bday day }

As a puzzle’s story proceeds, we track a changing “knowledge state”:

• A relation from characters to constants they’ve been given direct access to.

e.g., Albert → bday month, Bernard → bday day

• A “common knowledge” formula κ.

Logical encoding: evolving common knowledge

K_A,S(ϕ) means “character A in state S knows that ϕ”�KV_A,S(e) means “character A in state S knows the value of e”

Logical encoding: first-order knowledge

Z3 is only going to solve first-order formulas.

​

How to encode K_A,S(ϕ) in first-order logic?

K_A,S(ϕ) := ∀ (constants A doesn’t know in S) : κ_S → ϕ.

In other words,“A knows ϕ in state S iff ϕ is true in all worlds consistent with A’s knowledge in state S.”

​

How to encode KV_A,S(e) in first-order logic?

KV_A,S(e) := ∃v : K_A,S(e = v).

EpiPEn: A domain specific language in Python

Expressing puzzles

Operators that transform a (global) knowledge state:

announce(), learn_constant(), know(that=), know(value_of=), simultaneous(), …

Z3 API is used to for logical formulas (And, Not, …).

Python control structures can be used for complex puzzle constructions.

​

Solving puzzles

print_possible_worlds() calls Z3 to solve common-knowledge formula and list “possible worlds” (models).

EpiPEn: One example optimization

When A announces ϕ, we should add K_A,S(ϕ) to the common knowledge.

But what if ϕ = ¬KV_A,S(e)?

Turns out ¬KV_A,S(e) ↔︎ K_A,S(¬KV_A,S(e)).

“Negative introspection”: You know what you don’t know!

No reason to add extra layer of operators (with quantifiers, etc.)

​

EpiPEn always checks with Z3: ϕ ↔︎ K_A,S(ϕ)? If so, leave off the extra layer.

Over 100x speedup in some cases.

Applications

• A way for people to cheat at logic puzzles.
• A way for puzzle designers to more rapidly (& creatively?) explore the space of possible puzzles, looking for surprising new patterns.
• Use in linguistics, cryptography, ???