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). 也会普遍终止.

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

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

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

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

出于这样的原因,令人鼓舞的是,如果你只能展示(通常可以,也很容易)部分(1)终止,那么你的整个程序 - 第(1)部分和第(2)部分 - 也会终止.

你完全正确的是,任何可数无限的搜索空间都可以通过你描述的方式系统地覆盖到任何有限的范围.但是,这样做会破坏这种基本的不变性.您必须能够依靠以下财产才能申请上述推理:

label/1,labeling/2并indomain/1 始终终止.

在SWI-Prolog和YAP中,这是通过设计确保的.在其他系统中,它有不同程度的保持.