Solving a combinatorial puzzle with Clojure's core.logic

Posted on December 22, 2013

Recently I solved the following puzzle:

A prism with pentagons A₁ A₂ A₃ A₄ A₅ and B₁ B₂ B₃ B₄ B₅ as the top and bottom faces is given. Each side of the two pentagons and each of the 25 segments (A_i, B_j) is colored red or green. Every triangle whose vertices are vertices of the prism and whose sides have all been colored has two sides of a different color. Prove that all 10 sides of the top and bottom faces have the same color.

This problem was posed in the 1979 International Mathematical Olympiad and it admits a nice and short solution that I won’t spoil here. See the link for details.

I have been reading up on Clojure as well, and was waiting for an opportunity to experiment with it. Hence the decision to attack this problem using Clojure. One would perhaps use a SAT solver if an efficient solution is required, but let’s see how far we can get with Clojure.

I decided to use core.logic, a Clojure implementation of miniKanren. miniKanren is a logic programming language originally embedded in Scheme, but it has been ported to Clojure by David Nolen. A fairly readable introduction (and more, of course) to miniKanren can be found in William E. Byrd’s PhD thesis.

So first let’s define what it means for a triangle to have ‘two sides of a different color’. We’ll call such a triangle polychromatic.

(defn polychromatic
  [c0 c1 c2]
  (conde ((== [c0 c1 c2] [:green :green :red]))
         ((== [c0 c1 c2] [:green :red :green]))
         ((== [c0 c1 c2] [:red :green :green]))
         ((== [c0 c1 c2] [:red :red :green]))
         ((== [c0 c1 c2] [:red :green :red]))
         ((== [c0 c1 c2] [:green :red :red])))))

Let’s try to understand this definition. defn introduces a function that takes three arguments: three logic variables called c₀, c₁, c₂. The operator == unifies two expressions, who might contain logic variables. == works on vectors, lists, integers, hashmaps, keywords and possibly other values. conde is a macro and it corresponds to disjunction (logical ‘or’). The double parentheses threw me off in the beginning, but that’s because we can have multiple clauses per disjunction, who all must be true for that part of the disjunction to be true. As an example:

(defn adds-to-four 
  [x y]
  (conde ((== x 0) (== y 4))
         ((== x 1) (== y 3))
         ((== x 2) (== y 2))
         ((== x 3) (== y 1))
         ((== x 4) (== y 0))))

is a way to write the relation on the natural numbers (x, y) such that x + y = 4. It is also permitted to use vectors instead of lists, which is arguably clearer, like such:

(defn adds-to-four 
  [x y]
  (conde [(== x 0) (== y 4)]
         [(== x 1) (== y 3)]
         [(== x 2) (== y 2)]
         [(== x 3) (== y 1)]
         [(== x 4) (== y 0)]))

Now we will define two more useful relations. We will need a representation of the statement that side u of the pentagon p is colored c. Here u is an integer (0 ≤ u < 5), and p and c are logic variables.

(defn at
  [p u c]
  (fresh [c0 c1 c2 c3 c4]
         (== [c0 c1 c2 c3 c4] p)
         (== c ([c0 c1 c2 c3 c4] u))))

There is a new operator here, fresh, that takes a list of symbols and some clauses. This is the way to introduce fresh logic variables that have not yet been unified with anything. We’ll unify the pentagon p with [c0 c1 c2 c3 c4], and c with the u-th entry of that list.

We will represent the ‘intermediate edges’ (the edges going from the top to the bottom pentagon) with a vector of 5 pentagons. Slightly abusing at, we can then define at-int for integers u, v (0 ≤ u, v < 5) and logic variables p and c:

(defn at-int
  [p u v c]
  (fresh [int-c]
         (at p u int-c)
         (at int-c v c)))

Now define for integers u, v what it means for the two triangles connecting top-edges u, u+1, v and v + 1 to be polychromatic:

(defn succ [u] (mod (+ u 1) 5))

(defn triangle-polychromatic
  [prism [u v]]
  (fresh [top btm int c0 c1 c2 c3 c4]
         (== {:top top :btm btm :int int} prism)
         (at top u c1)
         (at btm v c2)
         (at-int int u v c0)
         (at-int int u (succ v) c3)
         (at-int int (succ u) v c4)
         (polychromatic c0 c1 c4)
         (polychromatic c0 c2 c3)))

In words, this first decomposes the prism into the top and bottom pentagons and the intermediate edges. We then find the colors of the two triangles:

c₀ is the color of the edge from top-vertex u to bottom-vertex v.
c₁ is the color of the edge from top-vertex u to top-vertex (succ u).
c₂ is the color of the edge from bottom-vertex v to bottom-vertex (succ v).
c₃ is the color of the edge from top-vertex u to bottom-vertex (succ v).
c₄ is the color of the edge from top-vertex (succ u) to bottom-vertex v.

Finally we state that the two triangles must be polychromatic.

We write down the conjunction of (triangle-polychromatic prism [u v]) for all u, v:


(def top-btm-edges (for [u (range 5), v (range 5)] [u v]))

(defn triangles-polychromatic
  [prism]
  (everyg (partial triangle-polychromatic prism) top-btm-edges))

We do not care about the intermediate edges, since the exercise only asks to prove a statement about the top and bottom pentagon. Therefore we write down that we are only interested in top and btm, where the prism is {:top top, :btm btm, :int int}:

(def solution (tabled [top btm] (fresh [prism int]
                                       (triangles-polychromatic prism)
                                       (== {:top top :btm btm :int int} prism))))

We use tabled to get rid of duplicate solutions. If we just use fresh there, we will get one solution for each assignment of the intermediate edges, even if we don’t see them.

Now we can finally instruct our computer to print the list of all solutions:

(run* [top btm] (solution top btm))

The core.logic operator run* returns all solutions: i.e., all assignments to the logic variables that satisfy the clauses.

When running, we get no surprises:

[[:green :green :green :green :green] [:green :green :green :green :green]]
[[:red :red :red :red :red] [:red :red :red :red :red]]

Running this program takes around 4 minutes, which is fairly slow (but considerably faster than most humans proving the statement). There is still quite some symmetry in the problem that has not been factored out, which might be the cause of the slowness. I have also noticed that logic programs are very sensitive to the order in which the clauses are written down (which is disappointing but understandable). I will need to understand the execution model of miniKanren / core.logic better.

The source code is available on Github.