prolog - 为什么在我添加冗余约束之前此 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 为非负时，不再有任何伪解，因此您的原始程序也会更好。