clojure - Clojure 中的目标排序 `core.logic`

Question

The following Clojure code使用 core.logic 以两种不同的顺序解决具有相同目标的相同逻辑问题。这种排序选择会导致一个很快完成，另一个则挂起。

(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]))))

是否有通用的解决方案或常见做法来避免此问题？

Answer 1

这是我的理解:

使用core.logic，您希望尽早减少搜索空间。如果您首先放置 membero 约束，则运行将通过搜索 membero 空间开始，并在 == 约束产生的失败时回溯。但 membero 空间是巨大的，因为 q 和 x 都不是统一的或至少是有界的。

但如果你把 == 约束放在前面，你就直接将 x 与 [1 2 3] 统一起来，搜索空间为membero 现在明确绑定(bind)到 x 的元素。