使用具体化约束使3个数字连续

Question

这是我的 SWI-Prolog 程序的概要：

:- use_module(library(clpfd)).

consec1(L) :-
   L=[L1,L2,L3,L4,L5,L6,L7,L8,L9],
   L ins 1..9,
   ...,
   abs(L5-L4)#=1,
   all_different(L),
   labeling([],L)

abs(L5-L4)#=1 使 L5 和 L4 彼此相邻。如果我想使三个数字彼此相邻，例如L3、L4 和 L5，我如何使用具体化的约束来做到这一点？

例如L3=4、L5=5、L4=6 或 L4=7、L5=8、L3=9

Answer 1

这实现了您在评论中给出的意义上的连续。对于 N 个值的列表，我们需要 space 足以使所有值介于两者之间，并且所有值都需要不同。

consecutive([]).  % debatable case
consecutive(Xs) :-
   Xs = [_|_],
   length(Xs, N),
   all_different(Xs),
   max_of(Max, Xs),
   min_of(Min, Xs),
   Max-Min #= N-1.

max_of(Max, [Max]).
max_of(Max0, [E|Es]) :-
   Max0 #= max(E,Max1),
   max_of(Max1, Es).

min_of(Min, [Min]).
min_of(Min0, [E|Es]) :-
   Min0 #= min(E, Min1),
   min_of(Min1, Es).

Answer 2

TL;DR: 评论太长：播放时间有专门的 sicstus-prolog clpfd 约束

此答案跟进； SICStus Prolog 的最新版本提供专门的 clpfd 约束 maximum/2 和 minimum/2 作为 min_of/2 和 max_of/2.

的替代方案

使用以下代码进行基准测试^1,2 ...

:- use_module(library(clpfd)).
:- use_module(library(between)).

bench_(How, N, Ub) :-
   \+ \+ ( length(Xs, N),
           domain(Xs, 1, Ub),
           all_different(Xs),
           Max-Min #= N-1,
           (  How = 0
           ;  How = min_of , max_of( Max, Xs), min_of( Min, Xs)
           ;  How = minimum, maximum(Max, Xs), minimum(Min, Xs)
           ),
           labeling([enum], Xs) ).

...我们运行进行了以下测试：

估计 min/max 约束的最坏情况开销：

?- member(How, [0,v1,v2]), (bench_(How,10,10), T_ms).
   How = 0 , T_ms =  5910
;  How = v1, T_ms = 19560
;  How = v2, T_ms =  7190.

要测量在更典型的情况下传播 min/max 约束的运行时间成本：

?- between(6, 8, N), NN #= N+N, call_time(bench_(v1,N,NN),T_ms).
   N = 6, NN = 12, T_ms =   50 
;  N = 7, NN = 14, T_ms =  300
;  N = 8, NN = 16, T_ms = 2790.

?- between(6, 8, N), NN #= N+N, call_time(bench_(v2,N,NN),T_ms).
   N = 6, NN = 12, T_ms =   20
;  N = 7, NN = 14, T_ms =  100
;  N = 8, NN = 16, T_ms =  830.

在这两个 "use cases" 中，专门的约束提供了令人印象深刻的加速。

^{脚注 1：使用 SICStus Prolog 版本 4.3.2（64 位）。

脚注 2：对答案序列进行了 post 处理以改善外观。}

使用具体化约束使3个数字连续

Use reified constraints to make 3 numbers consecutive

prolog

constraints

clpfd