7ML7W Minikanren Einsteins Puzzle

Following our last meeting about Minikanren, we decided we wanted to explore it some more through a more practical meeting. We decided to mob program a solution to Einstein's Puzzle (sometimes called the Zebra Puzzle) together:

Let us assume that there are five houses of different colors next to each other on the same road. In each house lives a man of a different nationality. Every man has his favorite drink, his favorite brand of cigarettes, and keeps pets of a particular kind.

• The Englishman lives in the red house.
• The Swede keeps dogs.
• The Dane drinks tea.
• The green house is just to the left of the white one.
• The owner of the green house drinks coffee.
• The Pall Mall smoker keeps birds.
• The owner of the yellow house smokes Dunhills.
• The man in the center house drinks milk.
• The Norwegian lives in the first house.
• The Blend smoker has a neighbor who keeps cats.
• The man who smokes Blue Masters drinks bier.
• The man who keeps horses lives next to the Dunhill smoker.
• The German smokes Prince.
• The Norwegian lives next to the blue house.
• The Blend smoker has a neighbor who drinks water.

The question to be answered is: Who keeps fish?

We started by reading the problem in more detail and immediately noted the potential complexity of relating houses as being to the "left" or "next to" one another and that the ultimate question asks about a pet that doesn't exist in any of the given facts.

Without a clear idea of how to proceed, we decided to try to solve a smaller problem (hereby refered to as Tuzz's Problem):

• There are three houses of different colours.
• The first house is red.
• The house next to the red house is blue.

Question: which house is green?

We wondered how best to state the above facts and how to represent houses, their relative positions and their colours. We started by defining our very own relation, coloro, for the first house:

(defn coloro [house color]
  (conde
    [(== house :first) (== color :red)]))

We could then use run to find the position of the red house:

(run* [q] (coloro q :red))
;=> (:first)

And double-check the colour of the first house:

(run* [q] (coloro :first q))
;=> (:red)

In order to express the position of the blue house, we needed to introduce another new relation, lefto, which we defined using db-rel and db we saw from last meeting:

(db-rel lefto a b)

(def facts
  (db
    [lefto :first :second]
    [lefto :second :third]))

We then defined the hilariously-named righto in terms of lefto:

(defn righto [a b]
  (lefto b a))

With these, we could now define the blue house:

(defn coloro [house color]
  (conde
    [(== house :first) (== color :red)]
    [(fresh [red-house]
            (lefto red-house house)
            (coloro red-house :red)
            (== color :blue))]))

(Side note: this took us a very long time to come up with. Originally we mixed up which house we were expressing goals about and using run just gave us bafflingly empty answers. After collectively staring at our code, quietly eating slices of olive bread and almost giving up entirely, a round of tactical commenting-out made us realise our mistake.)

Let's break this down:

First, we need a fresh variable for the house to left of this one and then we can use lefto to define the relative position of red-house and our current house:

(lefto red-house house)

Then we can define that the colour of red-house is, erm, red by recursively using our coloro relation:

(coloro red-house :red)

Finally, we need to say what the colour of our house must be if the house to our left is red:

(== color :blue)

Using our facts, let's answer some more questions:

(with-db facts (run 1 [q] (coloro :second q)))
;=> (:blue)
(with-db facts (run 1 [q] (coloro q :blue)))
;=> (:second)

Huzzah!

However, we became completely unstuck when trying to answer our ultimate question: where is that abominable green house?

We suspected that we were missing some way of expressing that there are exactly three houses and three colours but couldn't quite figure out how to represent it.

Over halfway through the meeting, we decide to consult an existing solution to the problem and were all agog at what we found there.

Putting aside the mysterious macro/symbol-macrolet incantation, we saw that houses were being represented as a vector of vectors. This is something @jcoglan had initially suggested and we decided to try to redo our implementation using this representation.

We were both surprised and disappointed that the way we'd need to answer questions would be to produce the full list of all houses (that is, we could no longer ask "which house is green?" but only ask "where are all the houses and what colours are they?"). Nevertheless, we decided to plumb on and replace our previous implementation with the following.

We first replace righto with a new relation that recursively defines that elements are left and right in a given list:

(defne righto [x y l]
  ([_ _ [x y . ?r]])
  ([_ _ [_ . ?r]] (righto x y ?r)))

We can then define the entire problem as a relation tuzzo that takes a vector of houses hs and, in order:

1. The first element in hs (the first house) is :red;
2. The house to the right of :red in hs is :blue;
3. There is a :green house in hs.

(defn tuzzo [hs]
  (all
    (fresh [a b]
      (== [:red a b] hs))
    (righto :red :blue hs)
    (membero :green hs)))

And with this, we can finally answer our question:

(run* [q] (tuzzo q))
;=> ([:red :blue :green])

Drunk on power, we decide to spice things up by adding pets to each house and the following new rules:

1. The green house has a dog;
2. The blue house has a parrot next door.

And a bold new question: where's the parrot?

To do this, we introduced a new relation nexto which used righto to relate to houses next to one another:

(defn nexto [x y l]
  (conde
    ((righto x y l))
    ((righto y x l))))

Then we could use this to express our new rules:

(defn tuzzo [hs]
  (all
    (fresh [a b c]
      (== [[:red a] b c] hs))
    (fresh [a b]
      (righto [:red a] [:blue b] hs))
    (fresh [a]
      (membero [:green a] hs))
    (fresh [a]
      (membero [:green :dog] hs))
    (fresh [a b]
      (nexto [:blue a] [b :parrot] hs))))

Now for the big reveal:

(run* [q] (tuzzo q))
;=> ([[:red :parrot] [:blue _0] [:green :dog]])

And to make things even more interesting, we removed the rule that the green house had a dog to produce two possible solutions:

([[:red :parrot] [:blue _0] [:green _1]]
 [[:red _0] [:blue _1] [:green :parrot]])

Contented, we pored through the full puzzle solutions implemented in various other programming languages on Rosetta Code.

References

• https://www.youtube.com/watch?v=1rDVz_Fb6HQ&vl=en
• https://web.stanford.edu/~laurik/fsmbook/examples/Einstein%27sPuzzle.html
• https://github.com/swannodette/logic-tutorial
• https://rosettacode.org/wiki/Zebra_puzzle

Thanks

Thanks to Elena and Unboxed for hosting the meeting and procuring large quantities of bread, thanks to Tom for bringing babas ganoush and various hummices and thanks to Simon for organising the meeting.