CLPFD 和无限可数域

Question

I #> 0, I #< 10, indomain(I).

前面的代码显然做了以下事情：

I = 1 ;
I = 2 ;
I = 3 ;
I = 4 ;
I = 5 ;
I = 6 ;
I = 7 ;
I = 8 ;
I = 9.

以下代码不起作用（参数没有充分实例化）：

I #> 0, indomain(I).

现在我了解到，在这种情况下，I 的可能绑定数量是无限的，而且 CLPFD 顾名思义适用于有限域。

但是我不明白为什么在这种特殊情况下存在这种限制。是不是可以从最小范数到最大范数列举出可能的解决方案，得到以下结果：

I = 1 ;
I = 2 ;
I = 3 ;
.
.
.

即使对于存在多个变量的问题，也可以说：

0 #< I, I #< J, label([I,J]).

为什么不能实现它，从而发生以下行为：

I = 1,
J = 2 ;
I = 1,
J = 3 ;
I = 2,
J = 3 ;
I = 1,
J = 4 ;
.
.
.

简而言之：如果无限域很容易使用幅度进行计数，为什么 CLPFD 仍然不能用于无限域？

Answer 1

这样做的原因是 CLP(FD) 保留了以下重要属性：

如果谓词p(Vs)普遍终止，那么?- p(Vs), label(Vs).也普遍终止。 p>

目标G 普遍终止 iff ?- G, false. 终止。

为什么这如此重要？因为 CLP(FD) 程序通常由两部分组成：

1. 发布所有限制
2. 寻找解决方案。

通过简单的检查，通常很容易表明建模部分 (1) 普遍终止。但是 (2) 是困难的部分，通常会占用大部分计算时间，而且我们通常先验知道是否存在单一解决方案。搜索部分可能会运行数天、数月或数年而没有产生结果。

许多 Prolog 初学者描述了一个搜索任务，运行它，几秒钟后抱怨 Prolog 很慢。事实上，事实证明，他们经常不小心编写了不会终止的程序，并且永远找不到解决方案。

出于这些原因，令人鼓舞的是，如果您只能显示（通常可以，而且相当容易）第 (1) 部分终止，那么您的整个程序 - 第 (1) 部分 和 第 (2) 部分——也终止。

您完全正确，任何可数无限搜索空间都可以通过您描述的一种方式系统地覆盖到任何有限范围。然而，这样做会破坏这个基本的不变量。要适用上述推理，您必须能够依靠以下属性：

label/1、labeling/2 和 indomain/1总是终止。

在 SWI-Prolog 和 YAP 中，这是通过设计确保的。在其他系统中，它在不同程度上成立。

Answer 2

没有理由在 CLP(FD) 中不允许无限域枚举。自从 由于 user:mat 已正确观察到约束本身终止，因此如果存在解决方案，则无限枚举可能会找到解决方案。

所以基本上我们有：

约束普遍终止，即 (#=)/2、(#=

然后我们观察：

约束的标签存在性终止，即它发现 如果我们还可以枚举多个 以公平的方式无限域。

所以主要问题是以公平的方式枚举多个无限域，因为当我们不以公平的方式枚举时，我们可能会误入该域的子集并且即使存在一个也找不到解决方案.想到以下枚举多个无限域的方法：

1) 取消配对功能
使用函数 unpair: N -> NxN，并仅枚举此函数的参数。这是此处描述的旧 Mathematica 技术：An Elegant Pairing Function。缺点是每次都要计算平方根。

2) 公平连接
使用公平的连接来组合无限的枚举数。这是一种应用于函数式编程的技术，请参见此处的示例：Backtracking, Interleaving, and Terminating Monad Transformers。缺点是连接词在恒定的内存空间中不起作用，您会产生越来越多的右侧枚举数实例。

3) 额外变量
使用额外的变量 H 和额外的约束，例如 H=abs(X1)+..+abs(Xn) 进行康托尔配对。然后，您可以枚举此变量并让约束求解器完成其余工作。对于某些值的优势，您可能会提前修剪。

在Jekejeke Minlog 中，我们最近选择了变体 3。这是一个枚举毕达哥拉斯三元组的示例：

?- use_module(library(finite/clpfd)).

?- [X,Y,Z] ins 1..sup, X*X+Y*Y #= Z*Z, label([X,Y,Z]).
X = 3,
Y = 4,
Z = 5 ;
X = 4,
Y = 3,
Z = 5 ;
X = 6,
Y = 8,
Z = 10 ;
X = 8,
Y = 6,
Z = 10 

一般来说，当使用无限标记时，我们会尝试解决Diophantine Equation，它并不总是有解决方案，甚至是不可判定的，我们在希尔伯特第十问题出现后就知道了。因此，甚至不可能保证通用终止。

另一方面，如果有解决方案，您可能会在一段时间后找到它，前提是该解决方案不太大，并且会超过计算机在内存空间和计算时间方面的限制。但这不应该让你的计算机崩溃，一个体面的 Prolog 系统实现应该优雅地回到顶层。您也可以打断口译员或停止要求进一步的解决方案。

再见