为什么在我添加冗余约束之前此 clpfd 查询不终止？

Question

我写了一些谓词，它们采用列表的长度并对其附加了一些约束（这是要使用的正确词汇表吗？）：

clp_length([], 0).
clp_length([_Head|Rest], Length) :-
  Length #>= 0, Length #= Length1 + 1,
  clp_length(Rest, Length1).

clp_length2([], 0).
clp_length2([_Head|Rest], Length) :-
  Length #= Length1 + 1,
  clp_length2(Rest, Length1).

第一个终止于这个简单的查询，但第二个没有：

?- Small in 1..2, clp_length(Little, Small).
Small = 1,
Little = [_1348] ;
Small = 2,
Little = [_1348, _2174] ;
false.

?- Small in 1..2, clp_length2(Little, Small).
Small = 1,
Little = [_1346] ;
Small = 2,
Little = [_1346, _2046] ;
% OOPS %

这对我来说很奇怪，因为长度明显大于 0。要弄清楚你可以搜索，找到零，并推断从零开始添加只能增加数字，或者你可以传播in 1..2 约束已关闭。感觉这个附加条款是多余的！这并不意味着我对 clpfd 的心理模型是完全错误的。

所以我想我有两个问题（希望对第二个问题的回答作为评论）

具体来说，为什么这个附加约束会导致查询正常工作？
一般来说，有没有我可以用来了解 clpfd 是如何实现的资源，而不是仅仅查看一些如何使用它的示例？我宁愿不必阅读 Markus Triska 的论文，但这是我能找到的唯一来源。如果我想回答这样的问题，这是我唯一的选择吗？

Answer 1

1mo，命名有问题。请参考之前的回答 mat me 推荐关系名称。使用不恰当的名称不会让您走得太远。因此 list_length/2 或 list_fdlength/2 将是一个合适的名称。因此我们有 list_fdlength/2 和 list_fdlength2/2.

2做，考虑list_fdlength2/2的规则。没有任何迹象表明 0 与您相关。因此，如果您使用 0 或 1 或 -1 或其他作为基本情况，则该规则将完全相同。那么这个糟糕的规则怎么会意识到 0 就是你的终点呢？更好的是，考虑一个概括：

list_fdlength2(fake(N), N) :-  % Extension to permit fake lists
   N #< 0.
list_fdlength2([], 0).
list_fdlength2([_Head|Rest], Length) :-
   Length #= Length1 + 1,
   list_fdlength2(Rest, Length1).

此概括显示了所有真实答案和虚假答案。请注意，我没有更改规则，我只是添加了这个替代事实。因此，假解实际上是由规则引起的：

?- list_fdlength2(L, 1).
      L = [_A]
   ;  L = [_A, _B|fake(-1)]
   ;  L = [_A, _B, _C|fake(-2)]
   ;  ...

?- list_fdlength2(L, 0).
      L = []
   ;  L = [_A|fake(-1)]
   ;  L = [_A, _B|fake(-2)]
   ;  ...

每个条款都试图在该条款的范围内为解决方案做出贡献。但是无法（通过内置的 Prolog 执行机制）推导出某些规则不再相关。你必须像你一样用冗余约束明确声明。

现在，回到包含冗余约束 Length #>= 0 的原始解决方案。根本不应该有任何这样的假解决方案。

list_fdlength(fake(N), N) :-
   N #< 0.
list_fdlength([], 0).
list_fdlength([_Head|Rest], Length) :-
   Length #>= 0,
   Length #= Length1 + 1,
   list_fdlength(Rest, Length1).

?- list_fdlength(L, 1).
      L = [_A]
   ;  L = [_A, _B|fake(-1)]   % totally unexpected
   ;  false.

?- list_fdlength(L, 0).
      L = []
   ;  L = [_A|fake(-1)]       % eek
   ;  false.

也有假答案！多么丑陋！至少，它们的数量是有限的。但是，你可以通过使用做得更好 Length #>= 1 代替 Length #>=0。有了这个小改动，当 N 为非负时，不再有任何伪解决方案，因此您的原始程序也会更好。

为什么在我添加冗余约束之前此 clpfd 查询不终止？

Why doesn't this clpfd query terminate until I add a redundant constraint?

prolog

clpfd