Loading [Contrib]/a11y/accessibility-menu.js
Download
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))