Exploring Logic Programming in Clojure’s core.logic – Finite Domain Constraints

In my last blog post, I went over a basic introduction to some of the concepts of logic programming. In this post, we’ll extend our last example to produce some real values (with meaning outside of the logic engine) using finite domain constraints.

Finite Domain Constraints?

The original miniKanren implementation only provides the ability to constrain your logic variables through unification. It’s easy to say that a logic variable must be a specific number: (== v 42). If you want to express that a logic variable must not be a specific number, but can still be anything else, then you’re out of luck. (As the combination of unification, conjunction, and disjunction is Turing complete, you will still be able to solve your problem, of course).

Over time, there have been extensions added to miniKanren to support what is called Constraint Logic Programming. Essentially, you can think of it as attaching clauses to a logic variable. Any attempt at unification must pass these clauses. The most basic constraint you can provide is disequality, which now makes the previous example possible: (!= v 42).

Naturally, Clojure’s core.logic supports CLP, and it also has an extension to describe constraints involving finite domains of numbers. This could be an interesting way to make our previous palindrome example more concrete, so let’s see if we can generate palindromes of integers whose sum is a specific value.

Using FD constraints

By convention, you’ll want to alias the clojure.core.logic.fd as fd, rather than intern its functions. Using it is straightforward enough. Before you begin applying finite domain constraints to a logic var, you must apply a domain using the fd/in function. Domains can be created using fd/interval and fd/domain. After that, there are functions for standard arithmetic operations.

Right as we start out, we have an interesting problem. Calling our palindromo goal will ultimately unify the supplied lvar with a list of some fresh lvars–the length of which will vary. Before we can begin constraining those lvars, we need to assign each one to a finite domain. If you’re reaching for doseq or map, wait a second! These are logic variables, not sequences. Instead, we’re going to have to deconstruct the contents of the palindrome using unification–in this case, conso.

(defn everyo [l f]
  (fresh [head tail]
    (conde
      [(== l ())]
      [(conso head tail l)
       (f head)
       (everyo tail f)])))

Now, applying a domain to the items of a palindrome becomes fairly simple:

  (palindromo q)
  (everyo q #(fd/in % our-domain))

Finally, we just need a goal to say that the sum of all the values in our palindrome must be a certain number. We can do this in a recursive style similar  to the way we implemented everyo:

(defn sumo [l sum]
  (fresh [a d sum-of-remaining]
    (conde
      [(== l ()) (== sum 0)]
      [(conso a d l)
       (fd/+ a sum-of-remaining sum)
       (sumo d sum-of-remaining sum)])))

The base case treats an empty list as if it has a sum of zero. For the recursive case, we utilize the constraint version of addition. Like our other logic programming goals, the “return” is another logic variable you must provide to its invocation. We say that the sum is the addition of the logic variable inside the first cell in the list plus an as-of-yet-undefined sum of remaining items. We promptly recurse to say that the sum of the rest of the list is that sum of the remaining items.

That’s pretty much it! To see it all in action, we just need to create a domain and  invoke our goals from run.

(defn find-palindromes-totalling [sum results]
  (let [domain (fd/interval 1 1000)]
    (run results [q]
      (palindromo q)
      (everyo q #(fd/in % domain))
      (sumo q sum))))

=> (find-palindromes-totalling 20 10)
((20) (10 10) (1 18 1) (2 16 2) (3 14 3) (4 12 4) (5 10 5) (6 8 6) (7 6 7) (8 4 8))

What happens if you request a large number of results? As it turns out, the program will hang forever (I think). Palindromes whose integer values total a given sum can only be, at most, as long as the sum is large. After it’s found (1 1 1 …. 1), palindromo will continue generating palindromes of ever-increasing length, and no real solutions will be found, despite everyone’s best efforts. Safeguarding against this case would be a good exercise for the reader.

Conclusion

With that, you’ve seen a nice cross-section of the features available in Clojure’s core.logic library, and hopefully you’ve  gained an understanding of how the core concept works in practice. I’ve found this exercise to be quite enjoyable, and I’m  keeping an eye open for ways it may be beneficial in the real world.

There are  obviously some small penalties of performance and familiarity, but it could be very interesting to deploy in a situation where you’re searching a logical problem space, or where you need to run an operation both forwards and backwards without writing it twice.