1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 | language Essence 1.3 $ prob024.essence: Langford's Number Problem $ Problem details available at http://www.csplib.org/Problems/prob024 $ numbers 1 to n, each appearing k times in a sequence (of length k*n) given k : int (2..) given n : int (1..) letting number be domain int (1..n) letting repetition be domain int (1..k) letting position be domain int (1..k*n) $ The positions of all repetitions of all numbers find pos : function ( total , injective ) tuple (number, repetition) --> position $ Occurrences of number i must be i+1 places apart. $ So if the number 4 appers at position 3, $ the next occurrence of it must be at position 8, $ leaving a gap of 4 positions. such that forAll i : number . forAll j : int (2..k) . pos( tuple (i,j)) = pos( tuple (i,j-1)) + i + 1 $ Symmetry breaking. $ The first occurrence of the number 1 is closer to the beginning than $ the last occurrence of the number 1 is to the end. such that pos( tuple (1,1)) - 1 < k*n - pos( tuple (1,k)) |