Solving Logic Puzzles With Clojure's Core Logic, Part Two

In part one we laid the foundations for solving logic puzzles with Clojure and core.logic. We built a core.logic query that encodes

rules of this particular puzzle, and come up with a solution.

The Rules

Let's recap the rules:

  1. Of Landon and Jason, one has the 7:30pm reservation and the other loves mozzarella.
  2. The blue cheese enthusiast subscribed to Fortune.
  3. The muenster enthusiast didn't subscribe to Vogue.
  4. The 5 people were the Fortune subscriber, Landon, the person with a reservation at 5:00pm, the mascarpone enthusiast, and the Vogue subscriber.
  5. The person with a reservation at 5:00pm didn't subscribe to Time.
  6. The Cosmopolitan subscriber has an earlier reservation than the mascarpone enthusiast.
  7. Bailey has a later reservation than the blue cheese enthusiast.
  8. Either the person with a reservation at 7:00pm or the person with a reservation at 7:30pm subscribed to Fortune.
  9. Landon has a later reservation than the Time subscriber.
  10. The Fortune subscriber is not Jamari.
  11. The person with a reservation at 5:00pm loves mozzarella.

When you look through them there are only really 5 kinds of rule in this puzzle, so we'll group them and tackle them in order of complexitye

Simple Facts

Rules (2) and (11) are the simplest:

* The blue cheese enthusiast subscribed to Fortune.
* The person with a reservation at 5:00pm loves mozzarella.

The first we handle by saying, "one of the answers - and we don't care which one - has the shape [* :fortune :blue-cheese *]. We handle * with an (lvar), and one-but-any-one with membero, to give us this:

  (defn rule-2
	"The blue cheese enthusiast subscribed to Fortune."
    [answers]
    (membero [(lvar) :fortune :blue-cheese (lvar)] answers))

In English, [* :fortune :blue-cheese *] is a member of the answer list.

That's fine, but I've a feeling we're going to be writing (lvar) a lot, so for rule 11 we'll start using clojure.tools.macro/symbol-macrolet for easier syntax:

  (defn rule-11
	"The person with a reservation at 5:00pm loves mozzarella."
    [answers]
    (symbol-macrolet [_ (lvar)]
                     (membero [_ _ :mozzarella 5] answers)))

Negated Facts

The second class of rules are negations:

  • The muenster enthusiast didn't subscribe to Vogue.
  • The person with a reservation at 5:00pm didn't subscribe to Time.
  • The Fortune subscriber is not Jamari.

Before we solve those, let's take a look at a naive first-pass that tripped me up:

  (defn BAD-rule-3
    "The muenster enthusiast didn't subscribe to Vogue."
    [answers]
    (symbol-macrolet
     [_ (lvar)]
     (not-membero (== [_ :vogue :muenster _] answers))))

not-membero isn't a built-in function of core.logic, but it's easy enough to find.

Sadly this doesn't work. It looks like it's saying, "Match a person who likes Vogue and muenster cheese and make sure it's not in the list of answers." But really it's saying, "Is it possible to construct a tuple that has Vogue and muenster, but isn't in the answer list?" That answer to that is, yes. [nil :vogue :muenster nil] would be such a tuple. So the rule is trivially and always true. In effect, it does nothing.

No, to encode these rules correctly we need to say something about what is in the answer list, and then make extra assertions about those things. We need to say, "There's a tuple with Vogue, a tuple with muenster, they're both in the answer list but they aren't the same tuple." Like this:

(defn rule-3
  "The muenster enthusiast didn't subscribe to Vogue."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (fresh [s1 s2]
          (== [_ :vogue _ _] s1)
          (== [_ _ :muenster _] s2)
          (membero s1 answers)
          (membero s2 answers)
          (!= s1 s2))))

That works. And note the use of fresh to introduce the named, local logic variables (magic boxes) we need.

Let's encode the other two rules of this type:

(defn rule-5
  "The person with a reservation at 5:00pm didn't subscribe to Time."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (fresh [s1 s2]
          (== [_ _ _ 5] s1)
          (== [_ :time _ _] s2)
          (membero s1 answers)
          (membero s2 answers)
          (!= s1 s2))))
(defn rule-10
  "The Fortune subscriber is not Jamari."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (fresh [s1 s2]
          (== [_ :fortune _ _] s1)
          (== [:jamari _ _ _] s2)
          (membero s1 answers)
          (membero s2 answers)
          (!= s1 s2))))

Related Pairs

The third class of rules relate pairs of facts:

  • Either the person with a reservation at 7:00pm or the person with a reservation at 7:30pm subscribed to Fortune."
  • Of Landon and Jason, one has the 7:30pm reservation and the other loves mozzarella.

For these we can use conde to make some OR statements. Here's the code for the first rule:

(defn rule-8
  "Either the person with a reservation at 7:00pm or the person with a
   reservation at 7:30pm subscribed to Fortune."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (fresh [r]
          (membero [_ :fortune _ r] answers)
          (conde [(== r 7)]
                 [(== r 7.5)]))))

This is saying, "There's an answer with Fortune in it, and I want to make a further assertion about the reservation, so name it r. My further assertion is, r is either 7pm or 7:30pm."

Fairly simple. And the next is only a little more complicated:

(defn rule-1
  "Of Landon and Jason, one has the 7:30pm reservation and the other loves mozzarella."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (fresh [c1 r1 c2 r2]
          (membero [:landon _ c1 r1] answers)
          (membero [:jason _ c2 r2] answers)
          (conde
           [(== r1 7.5) (== c2 :mozzarella)]
           [(== r2 7.5) (== c1 :mozzarella)]))))

This is saying, "There's an answer with Landon in, and I want to make some assertions about his choice of cheese & reservation. Ditto for Jasonjson." Then the assertions, "Either the first reservation is 7:30pm and the second cheese is mozarella, or the other way around."

Mutual Exclusion

Now we're on to the home straight. The next class of rules - actually there's only one of them - is a description of five separate tuples:

  • The 5 people were the Fortune subscriber, Landon, the person with a reservation at 5:00pm, the mascarpone enthusiast, and the Vogue subscriber.

The thing to notice here is that the rule's really saying, whoever has one trait in that list can't have any of the others. So we can use permuteo again to describe all 5 tuples, allowing for the facts to appear in any order:

(defn rule-4
  "The 5 people were the Fortune subscriber, Landon, the person with a
   reservation at 5:00pm, the mascarpone enthusiast, and the Vogue
   subscriber."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (permuteo [[_ :fortune _ _]
              [:landon _ _ _]
              [_ _ _ 5]
              [_ _ :mascarpone _]
              [_ :vogue _ _]]
             answers)))

Relative Facts

Okay, last class of rule:

  • The Cosmopolitan subscriber has an earlier reservation than the mascarpone enthusiast.
  • Bailey has a later reservation than the blue cheese enthusiast.
  • Landon has a later reservation than the Time subscriber.

These are all very similar to the related pairs above, but with a greater-than or less-than statement that makes things a little tricker. Actually, it makes things much trickier, as we can't just use < and > in core.logic.

I've taken an easy way out here. If I say that the reservation times are in strict order [5 6 7 7.5 8.5], then I can make greater-than and less-than statements by saying one is to the left of another.

I'll define to-the-left-of as this:

(defne lefto
  "x appears to the left of y in collection l."
  [x y l]
  ([_ _ [x . tail]] (membero y tail))
  ([_ _ [_ . tail]] (lefto x y tail)))

In English, "either x is the head of the list and y is a member of its tail OR drop the head and recur."

With that helper in place, the next three rules should look pretty clear:

(defn rule-6
  "The Cosmopolitan subscriber has an earlier reservation than the
   mascarpone enthusiast."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (fresh [r1 r2]
          (membero [_ :cosmopolitan _ r1] answers)
          (membero [_ _ :mascarpone r2] answers)
          (lefto r1 r2 [5 6 7 7.5 8.5]))))
(defn rule-7
  "Bailey has a later reservation than the blue cheese enthusiast."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (fresh [r1 r2]
          (membero [_ _ :blue-cheese r1] answers)
          (membero [:bailey _ _ r2] answers)
          (lefto r1 r2 [5 6 7 7.5 8.5]))))
(defn rule-9
  "Landon has a later reservation than the Time subscriber."
  [answers]
  (symbol-macrolet
   [_ (lvar)]
   (fresh [r1 r2]
          (membero [_ :time _ r1] answers)
          (membero [:landon _ _ r2] answers)
          (lefto r1 r2 [5 6 7 7.5 8.5]))))

Take It Home

That's it. Our driver function and our rules are all encoded. Running it produces a list containing a single answer:

(((:amaya  :fortune      :blue-cheese 7)
  (:bailey :vogue        :asiago      8.5)
  (:jamari :time         :mascarpone  6)
  (:jason  :cosmopolitan :mozzarella  5)
  (:landon :us-weekly    :muenster    7.5)))

On my machine it takes about 1s to find the first answer, and about 16s to search exhaustively (and thus demonstrate that one answer is all there is).

You can find the code on GitHub if you want to give it a whirl.

Thoughts? Questions? Suggestions? Leave a comment below...


  1. One of the hard parts of writing this code was typing Jason instead of JSON.