“最佳”方法取决于您的具体用例！这是另一种使用方法clpfd:
:- use_module(library(clpfd)).
我们定义谓词equidistant_stride/2正如@mat 在评论中所建议的相关问题的先前回答:
equidistant_stride([],_).
equidistant_stride([Z|Zs],D) :-
foldl(equidistant_stride_(D),Zs,Z,_).
equidistant_stride_(D,Z1,Z0,Z1) :-
Z1 #= Z0+D.
基于equidistant_stride/2，我们定义：
consecutive_ascending_integers(Zs) :-
equidistant_stride(Zs,1).
consecutive_ascending_integers_from(Zs,Z0) :-
Zs = [Z0|_],
consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
consecutive_ascending_integers_from(Zs,1).
让我们运行一些查询！首先，您的原始用例：
?- length(Zs,N), consecutive_ascending_integers_from_1(Zs).
N = 1, Zs = [1]
; N = 2, Zs = [1,2]
; N = 3, Zs = [1,2,3]
; N = 4, Zs = [1,2,3,4]
; N = 5, Zs = [1,2,3,4,5]
...
With clpfd，我们可以提出非常笼统的问题，并且也能得到逻辑上合理的答案！
?- consecutive_ascending_integers([A,B,0,D,E]).
A = -2, B = -1, D = 1, E = 2.
?- consecutive_ascending_integers([A,B,C,D,E]).
A+1#=B, B+1#=C, C+1#=D, D+1#=E.
的替代实现equidistant_stride/2:
我希望新代码能够更好地利用约束传播。
感谢@WillNess 提出了激发这次重写的测试用例！
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,N,D) :-
Z #= Z0 + N*D,
N1 #= N+1,
equidistant_from_nth_stride(Zs,Z0,N1,D).
equidistant_stride([],_).
equidistant_stride([Z0|Zs],D) :-
equidistant_from_nth_stride(Zs,Z0,1,D).
新旧版本与 @mat 的 clpfd 的比较：
首先是旧版本：
?- equidistant_stride([1,_,_,_,14],D).
_G1133+D#=14,
_G1145+D#=_G1133,
_G1157+D#=_G1145,
1+D#=_G1157. % succeeds with Scheinlösung
?- equidistant_stride([1,_,_,_,14|_],D).
_G1136+D#=14, _G1148+D#=_G1136, _G1160+D#=_G1148, 1+D#=_G1160
; 14+D#=_G1340, _G1354+D#=14, _G1366+D#=_G1354, _G1378+D#=_G1366, 1+D#=_G1378
... % does not terminate universally
现在让我们切换到新版本并提出相同的问题！
?- equidistant_stride([1,_,_,_,14],D).
false. % fails, as it should
?- equidistant_stride([1,_,_,_,14|_],D).
false. % fails, as it should
更多，现在，再来一次！我们可以通过尝试性地采用冗余约束来提前失败吗？
之前，我们建议使用约束Z1 #= Z0+D*1, Z2 #= Z0+D*2, Z3 #= Z0+D*3代替Z1 #= Z0+D, Z2 #= Z1+D, Z3 #= Z2+D（这个答案中的第一个版本的代码就是这样做的）。
再次感谢@WillNess 激发了这个小实验
注意到目标equidistant_stride([_,4,_,_,14],D)不会失败，而是会成功实现未完成的目标：
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D).
Zs = [_G2650, 4, _G2656, _G2659, 14],
14#=_G2650+4*D,
_G2659#=_G2650+3*D,
_G2656#=_G2650+2*D,
_G2650+D#=4.
让我们添加一些冗余约束equidistantRED_stride/2:
equidistantRED_stride([],_).
equidistantRED_stride([Z|Zs],D) :-
equidistant_from_nth_stride(Zs,Z,1,D),
equidistantRED_stride(Zs,D).
示例查询：
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D).
false.
完毕？还没有！一般来说，我们不想要二次数量的冗余约束。原因如下：
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D).
Zs = [_G2683, _G2686, _G2689, _G2692, 14],
14#=_G2683+4*D,
_G2692#=_G2683+3*D,
_G2689#=_G2683+2*D,
_G2686#=_G2683+D.
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D).
Zs = [_G831, _G834, _G837, _G840, 14],
14#=_G831+4*D,
_G840#=_G831+3*D,
_G837#=_G831+2*D,
_G834#=_G831+D,
14#=_G831+4*D,
_G840#=_G831+3*D,
_G837#=_G831+2*D,
_G834#=_G831+D,
D+_G840#=14,
14#=2*D+_G837,
_G840#=D+_G837,
14#=_G834+3*D,
_G840#=_G834+2*D,
_G837#=_G834+D.
但如果我们使用双重否定技巧，那么在成功的情况下，剩余部分仍然存在......
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
Zs = [_G454, _G457, _G460, _G463, 14],
14#=_G454+4*D,
_G463#=_G454+3*D,
_G460#=_G454+2*D,
_G457#=_G454+D.
... 和 ...
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
false.
...我们检测到的故障案例比以前更多！
让我们再深入挖掘一下！我们能否在更广泛的用途中及早发现故障？
根据目前提供的代码，这两个逻辑错误的查询不会终止：
?- Zs = [_,4,_,_,14|_], \+ \+ equidistantRED_stride(Zs,D), equidistant_stride(Zs,D).
... % Execution Aborted
?- Zs = [_,4,_,_,14|_], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
... % Execution Aborted
有修复吗？破解了！
?- use_module(library(lambda)).
true.
?- Zs = [_,4,_,_,14|_],
\+ ( term_variables(Zs,Vs),
maplist(\X^when(nonvar(X),integer(X)),Vs),
\+ equidistantRED_stride(Zs,D)),
equidistant_stride(Zs,D).
false.
该黑客行为并不能保证冗余约束“部分”的终止，但在我看来，对于快速的第一次射击来说，这还不算太糟糕。考试integer/1在实例化任何变量时Zs是为了允许clpfd求解器将变量域限制为单例，而 cons-pairs 的实例化（这直接导致基于列表的谓词的非终止）被抑制。
I do意识到黑客可以通过多种方式轻松破解（例如，使用循环术语）。欢迎任何建议和意见！
