使用Clingo ASP求解n=11的特殊排列序列问题

我正在学习ASP，需要寻找序列s=(s₁,s₂,…,s₁₁)，满足以下性质：

• s是集合{0,1,…,10}的排列；
• 序列v=(|s₂-s₁|,|s₃-s₂|,…,|s₁₁-s₁₀|)是集合{1,2,…,10}的排列。

我写了一段代码，但运行结果不符合预期，目前卡在正确建模的步骤上。

我的现有代码 #

% Define a sequence s = (s1, s2, ..., sn), n = 11, values between 0 and 10.
{s(N) : N=0..10}.

% Each number 0-10 has to occur exactly once.
1 { in(N) : s(N) } 1 :- N=0..10.

% I want s to be a permutation of {0,1,2,...,10} - how?
% ???

% Define a sequence v = (...), values between 0 and 10.
{v(M) : M=1..10}.

% Define the calculation of absolute differences between two adjacent elements of s.
diff(X, Y, D) :- v(X), v(Y), D = |X-Y|.

% Define a set of such differences.
abs_diff(D) :- diff(_, _, D).

% Each number 1-10 has to occur exactly once in that sequence.
1 { in_v(A) : v(A) } 1 :- A=1..10.

% v is a set of those differences.
v(X) :- abs_diff(X).

% Display results.
#show s/1.
#show v/1.

运行结果 #

程序返回错误输出：

v(1) v(2) v(3) v(4) v(5) v(6) v(7) v(8) v(9) v(10) v(0)
s(0) s(1) s(2) s(3) s(4) s(5) s(6) s(7) s(8) s(9) s(10)

我意识到自己没正确把s定义成集合的排列，只是把所有元素都列出来了，没有体现序列的顺序，也没把v和s的相邻元素关联起来。

我尝试过的错误方案 #

方案1：尝试用列表语法（无法运行） #

% Define the input set
set(0..10).

% Define the permutation predicate
perm([]).
perm([X|T]) :-
  set(X),
  select(X, Set, Rest),
  perm(T),
  Set = [X|Rest].
  
% Define the select predicate to choose an element from the set
select(X, [X|T], T).
select(X, [H|T], [H|T1]) :-
  select(X, T, T1).

报错信息

-:5:6-7: error: syntax error, unexpected [, expecting ) or ;

-:6:6-7: error: syntax error, unexpected [, expecting ) or ;

-:13:11-12: error: syntax error, unexpected [

-:14:11-12: error: syntax error, unexpected [

方案2：输出仍错误 #

1 { permute(I,D) : I=1..10, D=1..11 } 1 :-
  dif(1,1), dif(10,11),
  { permute(I,D) : I=1..10, D=1..11 } = 11,
  permutation(D, [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11]).

方案3：输出仍错误 #

#const n=11.

1 { s(X,Y) : Y=0..n-1 } 1 :- X=1..n.

:- s(X,Y), s(Z,Y), X!=Z.
:- s(X,Y), s(X,Z), Y!=Z.

正确解决方案 #

你之前的核心问题是：

1. 没有用带位置的谓词建模s的序列顺序（比如s(pos, value)，pos从1到11）；
2. 没有把v的元素和s的相邻位置关联起来；
3. 错误地用了ASP不支持的列表语法（ASP是基于谓词逻辑的，不是Prolog，不能直接用[X|T]这种列表结构）。

以下是针对n=11的正确ASP代码：

#const n=11.

% 1. 定义序列s：s(位置, 值)，位置从1到n，值从0到n-1
% 每个位置恰好选一个值
1 { s(P, V) : V=0..n-1 } 1 :- P=1..n.
% 每个值恰好出现在一个位置上
1 { s(P, V) : P=1..n } 1 :- V=0..n-1.

% 2. 定义相邻位置的绝对差v：v(位置差索引, 差值)，索引从1到n-1
% 计算每个相邻位置的差值，D是|s(P+1)-s(P)|
v(I, D) :- I=1..n-1, P=I, s(P, V1), s(P+1, V2), D = abs(V1 - V2).

% 3. 约束v的差值是1到n-1的排列
% 每个差值1..n-1恰好出现一次
1 { v(I, D) : I=1..n-1 } 1 :- D=1..n-1.
% 每个索引恰好对应一个差值
1 { v(I, D) : D=1..n-1 } 1 :- I=1..n-1.

% 展示结果：按位置顺序输出s，以及对应的v
#show s/2.
#show v/2.

代码解释 #

• 序列s的建模：用s(P, V)表示序列第P个位置的值是V，通过两个约束确保每个位置唯一值、每个值唯一位置，这样就保证了s是{0,..,10}的排列。
• 差值v的计算：遍历每个相邻位置对(P, P+1)，计算它们的绝对差，用v(I, D)表示第I个差值是D（I从1到10）。
• v的排列约束：同样用两个约束确保每个差值1..10恰好出现一次，每个索引对应唯一差值，保证v是{1,..,10}的排列。

运行结果示例 #

运行这段代码后，clingo会输出符合要求的解，比如其中一个解：

s(1,0) s(2,10) s(3,1) s(4,9) s(5,2) s(6,8) s(7,3) s(8,7) s(9,4) s(10,6) s(11,5)
v(1,10) v(2,9) v(3,8) v(4,7) v(5,6) v(6,5) v(7,4) v(8,3) v(9,2) v(10,1)

验证一下：s是0-10的排列，v的差值是10到1的排列，满足所有条件。

内容的提问来源于stack exchange，提问作者nooblet2