A greatly simplified version of https://github.com/tuzz/supersat

simplesupersat.rb

# This is a greatly simplified version of https://github.com/tuzz/supersat
# It reduces the superpermutation problem to boolean satisfiability.
#
# To generate a SAT problem for N=3, LENGTH=9:
# ruby simplesupersat.rb 3 9
#
# And to run a SAT solver on it:
# lingeling 3-9.dimacs

N = Integer(ARGV[0])
LENGTH = Integer(ARGV[1])

filename = "#{N}-#{LENGTH}.dimacs"
@file = File.open(filename, "w")

def next_variable
  @variable_count ||= 0
  @variable_count += 1
end

def variable(name)
  @variables ||= {}
  @variables[name] ||= next_variable
end

def clause(string)
  @clause_count ||= 0
  @clause_count += 1

  @file.print string
  @file.puts " 0"
end

# The input string has exactly one symbol at each time:
LENGTH.times do |time|
  symbols = N.times.map do |symbol|
    variable("Symbol_#{time}_#{symbol}")
  end

  # At most one:
  symbols.combination(2) do |(a, b)|
    clause "-#{a} -#{b}"
  end

  # At least one:
  clause symbols.join(" ")
end

# The input string starts with ascending numbers:
N.times do |time|
  clause variable("Symbol_#{time}_#{time}")
end

bits = Math.log2(LENGTH).ceil
max = 2 ** bits
permutations = 0.upto(N - 1).to_a.permutation.to_a

max.times do |position|
  binary = position.to_s(2).rjust(bits, "0")
  bools = binary.chars.map { |c| c == "1" }

  permutations.each do |perm|
    variables = bits.times.map do |bit|
      variable("Address_#{perm.join}_bit_#{bit}")
    end

    literals = variables.zip(bools).map do |v, b|
      "#{"-" if b}#{v}"
    end

    # Ban invalid addresses that go past the end of the input string:
    if position + N > LENGTH
      clause literals.join(" ")
      next
    end

    # The symbols for the permutation must be at that address in the string:
    perm.each.with_index do |symbol, i|
      time = position + i
      symbol = [variable("Symbol_#{time}_#{symbol}")]

      clause (literals + symbol).join(" ")
    end
  end
end

@file.close

File.open("#{filename}.tmp", "w") do |file|
  file.puts "p cnf #{@variable_count} #{@clause_count}"

  File.foreach(filename) do |line|
    file.puts line
  end
end

require "fileutils"
FileUtils.mv("#{filename}.tmp", filename)