Goal ordering in Clojure's `core.logic`

Question

The following Clojure code uses core.logic to solve the same logic problem with the same goals in two different orders. This choice of ordering causes one to finish quickly and the other to hang.

(use `clojure.core.logic)

;; Runs quickly.  Prints (1 2 3).
(clojure.pprint/pprint (run* [q] (fresh [x] (== x [1,2,3]) 
                                            (membero q x))))

;; Hangs
(clojure.pprint/pprint (run* [q] (fresh [x] (membero q x) 
                                            (== x [1,2,3]))))

Is there a general solution or common practice to avoid this problem?

Answer 1

If you're going to use membero there is no general solution to this problem. Calling membero with fresh vars will cause it to generate all (read, infinite) possible lists for which q is a member. Of course lists larger than 3 don't apply - but since you've used run* it will continue blindly trying lists larger than count 3 even though each one will fail.

It's possible to write a better version of membero in newer versions of core.logic using the constraint infrastructure, but the details of how one might do this are likely to change over the coming months. Until there's a solid public api for defining constraints you're stuck with the kind of subtle ordering and non-termination issues that trouble Prolog.

Answer 2

Here is my understanding:

With core.logic, you want to reduce the search space as early as possible. If you put the membero constraint first, the run will start by searching the membero space, and backtrack on failure produced by the == constraint. But the membero space is HUGE, since neither q nor x is unified or at least bounded.

But if you put the == constraint first, you directly unify x with [1 2 3], and the search space for membero now is clearly bounded to the elements of x.