024: Langford's number problem

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


$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$
$$$$$ MODEL 1: DIRECT
$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$


letting seqLength be k * n

$ The sequence of numbers
find seq : sequence (size seqLength) of int(1..n)

$ symmetry breaking
such that seq(1) < seq(seqLength)

$ Each number from 1 to n appear exactly k times in seq.
$ This constraint is implied, and it probably doesn't help search either.
such that
    forAll i : int(1..n) . |preImage(seq, i)| = k

$ Each occurrence of a number N is N positions apart.
$ 
$ So if the number 4 is at position 1 and if k=3,
$ then there has to be a 4 at position 6 and 11 as well.
such that
    $ for each number
    forAll number : int(1..n) .                     
        $ there exists a starting position 
        $ (i.e. the first position where number occurs)
        exists start : int(1..seqLength) .          
            $ positions start, start+(number+1), start+2*(number+1), ... 
            $ all contain the value "number"
            forAll i : int(1..k) . seq(start + (i-1) * (number+1)) = number


$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$
$$$$$ MODEL 2: POSITIONAL
$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$


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))


$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$
$$$$$ CHANNELLING
$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$

$ from pos to seq
such that
    forAll i : number .
        forAll j : repetition .
            seq(pos(tuple (i,j))) = i

$ from seq to pos
such that
    forAll i : int(1..k*n) .
        exists j : repetition .
            pos(tuple (seq(i),j)) = i

$ entries in pos are ordered
such that
    forAll i : number .
        forAll j : int(2..k) .
            pos(tuple (i,j-1)) < pos(tuple (i,j))

branching on [pos]