Clingo ASP - Define a sequence to be a permutation of a given set

Question

I am continuing my journey from here.

I am trying to learn ASP and working on a project like this:
Find the sequence s = (s1, s2, ..., sn) with the following properties:

• s is a permutation of the set {0, 1, ..., n-1};
• the sequence v = (|s2-s1|, |s3-s2|, ..., |sn-sn-1|) is a permutation of the set {1, 2, ..., n-1};

Solve this problem for n = 11.

I feel like I've made progress, but I am stuck now.

Here is the code I have:

% 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.

The program runs, but returns the wrong output: 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)

What I feel like I am missing is defining 's' to be a permutation of the set {0,1,2,...,10} instead of always being that set. But how can I do that?

I have tried the following solutions:

1. Does not run properly.

% 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. Output still wrong.

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. Output still wrong.

#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.

Any help is appreciated.

Answer 1

Welcome to asp.
So by reading through you code I guess it is best to show you some example code. To start of: in answer set programming, you work with sets of atoms. Therefore if you have a permutation you not only require the data but also its position. A choice rule {c(0..5)}. says that every possible c(N) may or may not be in the model. Try it from the webpage but choose enumerate all as mode: https://potassco.org/clingo/run/

Ok, how to encode a permutation? By defining predicates with arity 2: one for the position, one for the content

#const n=11.
% define constant n as  11

1 {s(P,V) : P = 0..n-1} 1 :- V = 0..n-1.  
% for every value V, V in exactly one position P 
% or more detailled: for every V, the number of atoms s(P,V) is exactly one

1 {s(P,V) : V = 0..n-1} 1 :- P = 0..n-1.  
% for every position P, P has exactly one value

Usually one of the two rules sufficies, but I like to write out both :)
Also please note you can reuse variable symbols in different rules.

Since v is also a permutation, you can define it just as such but for a different domain. Also please note v lacks one element in comparison to s

Now you need to link v and s togheter. Best choice is using constraints, since those do not add new atoms to the programm but can only reduce the number of potential answer sets. So what do we need? For any position P you need to know the fitting value in the permutation s and v and have them fullfill your equation.

:- P=1..n-1, s(P-1,S1), s(P,S2), v(P,V), not |S2-S1|=V.
% reads: it can not be that for any position P from 1 to n-1, 
% the fitting values in permutation s are S1 and S2, in v are V, 
% that |S2-S1| does not equal V.

Please note that the order of the atoms in the constraint does not matter and the reading is one of many interpretations of this rule.
And thats it. You can test your code on the clingo website.