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

原因是中电(FD)保留了以下重要属性：

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

目标G终止普遍当且仅当 ?- G, false.终止。

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

1. 张贴所有约束
2. 寻找解决办法。

通过简单的检查，通常很容易证明建模部分(1)是普遍终止的。但是(2)这是计算过程中最困难的部分，我们往往不知道是否存在单一的解。搜索部分可能运行数天、数月或数年而不会产生结果。

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

出于这些原因，令人鼓舞的是，如果您只能显示(通常情况下，也很容易)部分(1)终止，那么您的整个程序-部分(1)和部分(2)-also终止。

你是完全正确的，任何可数无限搜索空间都可以系统地覆盖到任何有限的程度，就像你所描述的方式之一。然而，这样做将打破这一基本不变。您必须能够依靠以下属性才能应用上述推理：

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

在和YAP中，这是通过设计来保证的.在其他系统中，它在不同程度上保持不变。

Answer 2

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

所以基本上我们有：

约束普遍终止，如(#=)/2、(#=<)/2等。在完全实例化时给出真或假，并且不要发散。

然后我们观察到：

约束的标号存在性地终止，即在一段时间后，如果我们还能公平地列举多个无限域，它就会找到一个问题的解决方案。

因此，主要的问题是公平地枚举多个无限域，因为当我们不以公平的方式枚举时，我们可能会在域的子集中误入歧途，即使存在这样的解决方案也找不到解决方案。列举多个无限域的方法如下：

1)解对函数

使用取消对:n -> NxN的函数，并仅枚举此函数的参数。这是这里描述的一种古老的数学技术：优雅的配对功能。缺点:每次都需要计算平方根。

2)公平连接

使用公平的连词组合无限枚举数。这是一种应用于函数式编程的技术，参见这里的回溯、交织和终止Monad变压器。缺点--连接不能在常量内存空间中工作，您将生成越来越多的右侧枚举器实例。

3)额外变量

对cantor配对使用额外的变量H和额外的约束，例如H=abs(X1)+..+abs(Xn)。然后，您可以枚举这个变量，并让约束求解器完成其余的工作。某些值的优势，您可能有早期剪枝。

在杰基耶克·明洛中，我们最近选择了变体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 

一般情况下，当使用无限标号时，人们会尝试求解一个丢番图方程，它并不总是有一个解，甚至是不可判定的，这一点我们在希尔伯特第十个问题出现后就知道了。因此，保证普遍终止甚至是不可能的。

另一方面，如果有一个解决方案，您可能会在一段时间后找到它，只要解决方案不太大，并且将超过计算机在内存空间和计算时间上的限制。但这不应该使你的计算机崩溃，一个像样的Prolog系统实现应该优雅地回到顶层。您也可以中断解释器或停止要求进一步的解决方案。

再见