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
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/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
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,
(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
(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.
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.