SAT: Langford Pairs

I set up a SAT to solve the Langford Pairs Problem. Definition:

Given a natural number n, order the 2n numbers [1, 1, 2, 2, ..., n, n] in such a way that the two instances of any number k has exactly k numbers between them in the sequence.

The solution for n=3:

3, 1, 2, 1, 3, 2

The solution to the SAT modelling of this is given on page 5 of Knuth's satisfiability. I implemented this as:

For this, I have wrapped pysat.solvers.Solver, so that it keeps track of which variable names have been used (variable names are stored as integers). I also added the constraint symmetric. A symmetric constraint means that exactly one of the variables should be True. For n=12 the solution is:

7, 4, 11, 5, 6, 9, 4, 10, 7, 5, 12, 6, 8, 3, 11, 9, 2, 3, 10, 2, 1, 8, 1, 12

I call the wrapper SugarRush. This is a reference to the Glucose SAT solver, which is the default [1][2]. It is also a reference to syntactic sugar.

[1] The Glucose SAT Solver
[2] Audemard, Gilles, and Laurent Simon. "GLUCOSE: a solver that predicts learnt clauses quality." SAT Competition (2009): 7-8.