FD逻辑并不总是返回所有解

Question

以下代码


(run* [x11 x12 x13
       x21 x22     x24
       x31     x33 x34
           x42 x43 x44]
      (fd/in x11 x12 x13 x21 x22 x24 x31 x33 x34 x42 x43 x44 (fd/interval 1 9))
      (fd/eq (= (+ x11 (/ x12 x13))   5)
             (= (+ x21 (/ x22   2)) x24)
             (= (+ x31 (/   6 x33)) x34)
             (= (+   4 (/ x42 x43)) x44)
             (= (+ x11 (/ x21 x31))   4)
             (= (* x12 (/ x22   6)) x42)
             (= (+ x13 (-   2 x33)) x43)
             (= (+ (-  5 x24) x34)  x44)))


我的结果是 {{([1 4 1 3 6 6 1 1 7 4 2 6] [2 6 2 4 6 7 2 1 8 6 3 6])}}。

然而，只要我将 {{(fd/interval 1 9)}} 更改为 {{(fd/interval 0 9)}}, 结果就成为一个空序列。然而，我预期它将包含上述两个解决方案至少之一。

Answer 1

评论者：dnolen

如果您能确认在没有使用{{fd/eq}}的情况下存在此问题将很有帮助 - 它仅仅是宏糖衣。写出长形式会很麻烦，但将有助于隔离问题。谢谢。

Answer 2

评论人：dnnx

我怀疑这个bug出在 fd/eq 中。这里是一个更小的测试案例

`
(run* [q]

  (fd/in q (fd/interval 1 2))
  (fd/eq (= (/ q q) 1)))

`

它返回预期的 (1 2)，但我将 fd/interval 更改为 0 2 后，它返回一个空序列。

Answer 3

评论者：dnolen

感谢你提供了最小化案例，看起来确实有 {{fd/eq}} 的问题，因为它用长格式写入时运行正常。

Answer 4

评论者：dnolen

另请参阅 LOGIC-156

Answer 5

参考：[https://clojure.atlassian.net/browse/LOGIC-162](https://clojure.atlassian.net/browse/LOGIC-162) (由 alex+import 报告)