具有 -ve 值的 Core.logic 有限域答案

【问题标题】：Core.logic finite domain with -ve values具有 -ve 值的 Core.logic 有限域
【发布时间】：2012-11-02 12:43:35
【问题描述】：

我不确定为什么使用 -5 作为域值之一时下面的代码没有返回任何结果

user=> (run* [q] (infd q (domain -5 5)) (*fd q q 25))
()
user=> (run* [q] (infd q (domain 0 5)) (*fd q q 25))
(5)

注意：此代码指的是 core.logic 0.8.0 测试版中的行为。

【问题讨论】：

标签： clojure clojure-core.logic

【解决方案1】：

目前在 core.logic 0.8.0 测试版中根本不支持负值域。如果它起作用，那完全是偶然的。我不打算在不久的将来亲自添加对此的支持，尽管在 0.8.0 获得适当的版本后欢迎提供全面的补丁。

【讨论】：

不，这需要支持对实数的约束逻辑编程，CLP(R)。绝对有兴趣为此做出贡献，但这也不是我打算自己做的事情。

【解决方案2】：

看起来*fd 约束的实现只适用于所有正值的域。它基于乘积域的下限/上限除以右手因子域的上限/下限来计算左手因子的上限和下限，反之亦然。您可以看到将底片混入其中会导致此方法不起作用：

 (run* [q]
   (fresh [r]
     (infd q (domain 1 2 3 4 5))
     (infd r (domain 20 25))
     (*fd q q r)))

 Product = [20..25], RHS = [1..5] => LHS = [20/5..25/1] = [4..25]

 (run* [q]
   (fresh [r]
     (infd q (domain -1 0 1 2 3 4 5))
     (infd r (domain 20 25))
     (*fd q q r)))

 Product = [20..25], RHS = [-1..5] => LHS = [20/5..25/-1] = [4..-25]

由于标志已关闭，因此 LHS 的区间最终无法满足，因为下限大于上限。

具有负值的有限域确实适用于 +fd 约束：

 (run* [q] (fresh [a b] (infd a b (domain -1 0 1)) (+fd a b 0) (== q [a b])))
 => ([-1 1] [0 0] [1 -1])

【讨论】：