模函数和变域

Question

这是一个简单的 CLPFD 关系：

1 #= 81 mod X.

这个returns:

X in inf.. -1\/1..sup,
81 mod X#=1.

除非我的数学完全不正确，否则 X 的域不应该是 -80.. -1\/1..80 吗？

Answer 1

要事第一：

Is there a mistake in the constraint solver?

没有（不一定），因为所有可采纳的解仍然包含在推导的域中，没有报错解。您推导的域是求解器报告内容的适当子集。

Does the constraint solver propagate as well as it could in this case?

否，显然不是，因为您的更强边界已经显示出来。事实上，容许域比你推断的还要小：X in 2..80 会也是有效的，因为 X 肯定不是是负数，它也不能等于 1。

练习：在这种情况下，X in 2..80是最小的（关于集合包含）域吗？为什么不）？如果有的话，在什么意义上是它是最小的？

So, what is going on here?

解释相当简单：实施 (mod)/2、(rem)/2、(div)/2 并且——在较小程度上——甚至 (*)/2 以这样一种方式传播 尽可能在所有情况下都非常困难，并且在这种情况下显然没有做到。

Do we have to live with this shortcoming?

否，因为我们也可以改进约束求解器来处理此类情况！也就是说，我们可以添加逻辑，使其传播更强烈！优雅而正确地做到这一点通常是一个 未解决的问题 ，并且是 积极研究 的主题。例如，参见 Finite Domain Constraint Solver Learning、其中包含的参考文献和其他几篇论文。当然，梦想是以某种方式直接从这些操作的规范中导出传播，这至少需要几十年的时间。在此之前，此类问题会被发现并得到改进，而不是临时。

Answer 2

免责声明：我不知道我在说什么，我只是想亲眼看看会发生什么，并认为分享可能有用。

使用 SWI-Prolog 和库 (clpfd)：

?- use_module(library(clpfd)).
true.

?- 1 #= 81 rem X.
X in inf.. -1\/1..sup,
81 rem X#=1.

?- 1 #= 81 mod X.
X in inf.. -1\/1..sup,
81 mod X#=1.

?- 1 #= 81 - X * (81 // X ).
X in -80.. -1\/1..80,
X*_G1053#=80,
81//X#=_G1053,
_G1053 in -80.. -1\/1..80.

奇怪，上个例子的表达式不应该是模除法的定义吗？

如果你使用 Gnu-Prolog（mod 不直接支持）：

| ?- 1 #= 81 rem X.

X = _#4(2..80)

yes
| ?- 1 #= 81 - X * (81 // X).

no

嗯。如果您只是 重新排序表达式 :

会怎么样

| ?- 1 #= 81 - (81 // X) * X.

X = _#4(2..80)

yes

结论：是的，看来写一个好的CLP(FD)库确实不容易。甚至可能会给人留下这样的印象，即这些库表现出作者并不总是完全意识到的紧急行为。

模函数和变域

Modulo function and variable domain

prolog

clpfd