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 (由 alex+import 报告)