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:

	def langford(solver, n):
	X = [[solver.var() for _ in range(2*n - k - 2)] for k in range(n)]
	for row in X:
	solver.symmetric(row)
	position2covering = defaultdict(list)
	for k, row in enumerate(X):
	for i, var in enumerate(row):
	position2covering[i].append(var)
	position2covering[i + k + 2].append(var)
	for lits in position2covering.values():
	solver.symmetric(lits)
	solver = SugarRush()
	langford(solver, 12)
	solver.solve()

view raw langford.py hosted with ❤ by GitHub

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.