Reduce the problem of finding superpermutations of N digits to SAT

superpermutation.rb

# Attempts to find a superpermutation for a given number of digits that fit into a given string length.
# https://en.wikipedia.org/wiki/Superpermutation
#
# Run: ruby superpermutation.rb | lingeling -f
#
# The program will be satisfiable if it is possible, but won't actually print the solution.
# I need to add some code to decode the output.

digits = 4
length = 33

def write(string)
  if ENV["DEBUG"]
    print string
  else
    print string.gsub(/[^\s-]+/) { |s| lookup(s) }.gsub("\n", " 0\n")
  end
end

def lookup(name)
  @registry ||= {}
  @registry[name] ||= @registry.size + 1
end

permutations = digits.times.to_a.permutation(digits)
limit = length - digits + 1

length.times do |l|
  digits.times do |d|
    write "L_#{l}_#{d} "
  end
  write "\n"

  digits.times.to_a.combination(2).each do |a, b|
    write "-L_#{l}_#{a} -L_#{l}_#{b}\n"
  end
end

limit.times do |l|
  permutations.each do |perm|
    perm.each.with_index do |p, i|
      write "-P_#{l}_#{perm.join} L_#{l + i}_#{p}\n"
    end
  end
end

permutations.each do |perm|
  limit.times do |l|
    write "P_#{l}_#{perm.join} "
  end
  write "\n"
end