Download
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 [seq]